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

Авторы: Коллаборация 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]