Онлайн-сообщество недавно определило BB(5) = 47,176,870, первый большой прорыв в проблеме "busy beaver game" за 50 лет. Следующая цель - BB(6), но исследователи не ожидают её достижения в ближайшее время из-за программы Antihydra, которая напоминает нерешенную математическую проблему Collatz conjecture.

Busy beaver numbers измеряют сложность вычислений, которые могут выполнить простые компьютерные программы. В этих исследованиях программы представлены машинами Тьюринга - гипотетическими устройствами, считывающими и записывающими 0 и 1 на бесконечной ленте. Каждая машина имеет уникальный набор правил, определяющих её поведение.

Antihydra представляет особую сложность, так как её поведение тесно связано с проблемой Collatz conjecture, одной из самых известных нерешенных задач в математике. Эта связь делает BB(6) практически недостижимым для точного определения в обозримом будущем.

• Обсуждение охватывает от Busy Beaver до Collatz, от теории вычислимости до философии случайности и даже до SETI@home и Bitcoin, показывая, насколько широко разросся этот меметический вирус.
• Участники обсуждают, как быстро растет функция BB(n), и как она влияет на наше понимание пределов вычислимости и случайности.
• Обсуждается, что даже если бы мы знали BB(5) или BB(6), это бы не дало нам практического способа вычислить BB(6) или выше; вопрос остаётся открытым, что делает эту область столь интригующей.
• Участники также затрагивают вопрос о том, как публикация в блогах может влиять на восприятие этой темы и как можно было бы лучше донести эти идеи до широкой аудитории.
• В конце обсуждение смещается к тому, что даже если бы мы могли бы вычислить эти числа, мы бы всё равно не могли бы их сравнить с чем-то, потому что они бы оказались слишком большими, чтобы иметь какое-либо значение в контексте чего-либо, кроме как самоограничения.

Определение пятого значения функции занятого бобра

Авторы: Коллаборация bbchallenge (Джастин Бланшар и др.)

Аннотация: Мы доказываем, что $S(5) = 47,176,870$ с использованием системы проверки доказательств Coq. Значение занятого бобра $S(n)$ — максимальное число шагов, которое машина Тьюринга с $n$ состояниями и 2 символами может выполнить с нулевой ленты до остановки. Функция $S$ была введена Тибором Радо в 1962 году как один из простейших примеров невычислимой функции. Доказательство включает перебор $181,385,789$ машин Тьюринга с 5 состояниями и определение для каждой из них, останавливается ли она. Наш результат — первое определение нового значения занятого бобра за более чем 40 лет и первое формально верифицированное значение, что демонстрирует эффективность массовых онлайн-исследований (bbchallenge$.$org).

Комментарии: 48 страниц, 17 рисунков

Предметные области: Логика в информатике (cs.LO); Формальные языки и теория автоматов (cs.FL); Логика (math.LO)

Цитирование: arXiv:2509.12337 [cs.LO]

• Результат BB(5) был подтверждён с использованием комбинации исчерпывающего перебора и продвинутых методов анализа (десидеров) для проверки остановки машин Тьюринга.
• Процесс проверки был значительно оптимизирован: большинство машин было отсеяно на ранних этапах, и лишь 183 машины потребовали глубокого моделирования (до 47 млн шагов).
• Исследование является крупным collaborative-проектом с открытым исходным кодом, аналогичным другим сообществам, изучающим клеточные автоматы и гугологию.
• Значение BB(5) само по себе не имеет прямого практического применения и считается чисто академическим достижением, однако разработанные методы могут быть полезны для статического анализа программ и решения проблем остановки.
• Некоторые машины Тьюринга, включая кандидата для BB(6), выполняют вычисления, аналогичные последовательности Коллатца, что представляет отдельный математический интерес.
• Проверка доказательства с помощью Coq требует нескольких часов на обычном компьютере, что несопоставимо с вычислительными затратами на его получение.
• Для машин с большим числом состояний (начиная с BB(6)) прямое вычисление значения считается невозможным из-за его колоссального размера и неразрешимости проблемы остановки в общем случае.

• Критика стиля и содержания поста Вольфрама: много визуализаций без ясной цели, изобретение непонятного термина "ruliology", самопрезентация автора.
• Положительные отзывы: пост как хорошее введение в лямбда-исчисление, демонстрация ценности визуализации даже абстрактных концепций, стимулирующий и ясный стиль написания.
• Сравнение с другими систематическими работами: упоминание функционального аналога "занятого бобра" (A333479) и вопроса о простоте анализа по сравнению с машинами Тьюринга.
• Обсуждение целевой аудитории: пост написан не для инженеров-программистов, а для физиков и математиков, изучающих вычисления.
• Упоминание концепций Вольфрама: "ruliad" (вселенная как программа) и "ruliology" как их изучение, переоткрытие тезиса Чёрча-Тьюринга.

Что такое «Busy Beaver»
Функция Σ(n) показывает максимальное количество 1, которое может оставить на ленте останавливающаяся машина Тьюринга с n состояниями и двумя символами (0 и 1). Аналогично, S(n) — максимальное число шагов до остановки. Оба значения растут быстрее любой вычислимой функции, поэтому уже Σ(5) и S(5) неизвестны без компьютерного перебора.

Новый рекорд: n = 6
Команда «Beaver Hunters» (Scott Aaronson, Shawn Ligocki et al.) доказала:

• S(6) = 36 534 678 263 377 ≈ 3,65 × 10¹³
• Σ(6) = 10 ↑↑ 15
  (15-я степень десятки в стеке степеней: 10^(10^(10^…)))

Это число настолько велико, что его нельзя записать в обычной десятичной форме: для этого потребовалось бы больше атомов, чем во Вселенной.

Как нашли

• Использовали SAT-решатели и распределённые вычисления, чтобы перебрать ~10⁴⁴ машин.
• Для оставшихся «подозрительных» случаев построили индивидуальные доказательства остановки или бесконечного цикла.
• Работа заняла ~2 года и миллионы часов CPU.

Зачем это нужно

• Busy Beaver служит «натуральной» границей между вычислимым и не-вычислимым.
• Новые методы перебора и доказательств могут пригодиться в верификации ПО и теории сложности.
• Следующая цель — n = 7, но она потребует принципиально новых идей и, вероятно, ещё более фантастических чисел.

• Участники обсуждают сверхбольшие конечные числа: Busy Beaver, TREE(3), субкубические графы и быстро-растущие иерархии.
• BB-функция растёт быстрее любой вычислимой функции и не вычислима; для N>549 нельзя доказать в ZFC, что какое-то вычислимое число ≥BB(N).
• Поделились ссылками на видео Numberphile, плейлист Дэвида Мецлера и статью Скотта Ааронсона.
• Появились размышления о том, что делает такие числа интереснее бесконечности, а также о состоянии ленты после остановки BB(5).
• Некоторые критикуют статью Quanta за поверхностное описание экспоненциации и отсутствие объяснения сути BB.