# Пост: Занятой бобёр вышел из-под контроля: 10 состояний против числа Грэма
# Пост: Занятой бобёр вышел из-под контроля: 10 состояний против числа Грэма Десять состояний, два символа — и число, рядом с которым число Грэма выглядит скромной сноской. Новая машина Тьюринга сделала именно это. Занятой бобёр — задача с простыми правилами и чудовищным поиском. Берём машину Тьюринга с фиксированным числом состояний, запускаем на пустой ленте и ищем ту, что оставит максимум единиц перед остановкой. Для десяти состояний точное значение BB(10) неизвестно. Новый рекордсмен лишь поднял нижнюю границу. Джефф Кетчерсид нашёл машину компьютерным перебором 8 октября. Проверка в Coq подтверждает: она останавливается, обходит предыдущего кандидата и оставляет больше единиц, чем число Грэма. Предыдущий рекорд 2024 года достигал уровня fω(fω(25)) в иерархии быстрорастущих функций. Новая конструкция поднялась до fω+1 — рост качественно быстрее. Машина основана на восьми состояниях. Кетчерсид добавил два: они перехватывают момент остановки и запускают новые циклы, каждый раз раздувая уже огромное значение. Это самая маленькая известная двухсимвольная машина, перешагнувшая границу числа Грэма. Раньше для такого масштаба требовалось минимум 13 состояний. Точное число шагов пока не вычислено. Но чтобы записать столько единиц, шагов нужно больше числа Грэма. Формальное доказательство построено без дополнительных аксиом, однако независимой проверки сообщества ещё не было. Так что это опубликованный рекорд и более высокая нижняя граница, а не окончательное BB(10). Почему это важно? Это наглядный предел формальных методов и сложности вычислений. Простые правила могут порождать поведение, которое невозможно уместить в голове. Для разработчиков это напоминание: остановка программы — фундаментально тяжёлая задача, и даже 10 состояний уже требуют машинно-проверяемых доказательств. --- **Мнение DevGeek.IT** Меня здесь впечатляет не число Грэма, а дисциплина доказательства: Coq, отсутствие лишних аксиом, аккуратная формулировка «нижняя граница», а не «точное значение». Это правильный способ делать сенсации в математике. Но без независимой проверки я бы не спешил называть рекорд окончательным. Если десять состояний дают такую бездну, что уж говорить о реальном коде на миллионы строк. Как думаете, докажем ли мы когда-нибудь остановку хотя бы для всех программ до 20 состояний? --- #DevGeekIT #BusyBeaver #Тьюринг #Coq #Математика #Вычисления