Так вот оказывается, что если копнуть чуть-чуть поглубже, то выясняется что это всё — огромный фейк ☠️

Сперва надо было классифицировать все 63,403,380,965,376 возможных 5-состояний машин Тьюринга. Затем надо было сам алгоритм моделирования машины Тьюринга запустить, соответственно, 63+ триллиона раз, применить эвристики быстрой классификации, и отобрать кандидаты с максимальными значениями.

Так вот сермяга в том, что 99.9% бобров классифицируются быстрыми эвристиками, а отнюдь не формально верифицированными доказательствами.

В чём же тогда заключается "доказательство" BB(5)?

"Решение" BB(5) = 47,176,870 основано на:
✓ формально верифицированных алгоритмах (~1% работы)
? эвристиках быстрой классификации (~98% работы)

Да, но отсутствие багов в коде? Корректность аппаратуры? Корректность самих эвристик? Нет, конечно.

Полностью верифицированные формальные доказательства строились на Coq только для самых трудных единичных случаев (особенно для доказательства незавершимости). Например с огромным трудом удалось доказать (или опровергнуть), что самый проблемный бобёр (1RB 1LC 1RC 1RD 1LA 1LA 1RB 1RH 0LE 1LB) никогда не достигает состояния HALT.

Корректность реализации симулятора, что он корректно выполняет переходы (так-то это 15 строк на питоне, разберём их верификацию в моём гайде:), доказывалось на Isabelle.

Алгоритмы обнаружения циклов и квази-поведения формально верифицировались на Lean.

Ну и всё. Всё остальное 98% — чистая программная инженерия.

Эвристика: "Машина зациклилась после 1000 шагов"
Реальность: Машина остановится через 10^100 шагов
Результат: Пропустили рекордсмена! 🙈

=

Короче говоря единственное что можно сказать — это чисто инженерное решение с некоторыми математическими гарантиями.

— BB(5) ≥ 47,176,870 (это точно доказано)
— Существует 5-машина, которая производит именно 47,176,870 единиц.

И не более. Конечно, на 99,98% скорее всего именно так и есть — и всё же...

=

Требуемое моделирование с множеством эвристик – это не недостаток методов, а неизбежное следствие природы вычислений. Из-за фундаментальных теорем неразрешимости (Райс, проблема останова) это области, где интеллектуальный перебор, глубокий анализ конкретных случаев и изобретательные эвристики — единственный практический путь вперёд 💪🏻

Достижения в вычислении BB(5) и начавшиеся атаки на BB(6) — это триумф человеческой изобретательности в преодолении принципиальных математических барьеров 🚀

А зачем вообще люди занимаются этим, насколько это подобное вообще "серьёзно" ?
Ну, не более серьезно, чем 98% всей теоретической математики :)