Теренс Тао делится предварительными соображениями о текущих усилиях по формализации математики с использованием ИИ и языковых моделей. Он отмечает, что хотя автоматизированные системы доказательств, такие как Lean, уже способны проверять сложные математические утверждения, генерация оригинальных доказательств и интуитивных идей остаётся сложной задачей. Тао подчёркивает важность симбиоза между человеческой креативностью и машинной точностью, где ИИ помогает устранять ошибки и предлагает возможные пути решения, но ключевые прорывы по-прежнему исходят от математиков.

Он также указывает на практические ограничения: текущие ИИ-инструменты часто требуют значительной ручной настройки и могут генерировать избыточные или неэффективные доказательства. Однако их способность быстро перебирать огромное количество вариантов делает их незаменимыми помощниками в проверке гипотез и поиске контрпримеров. Тао ожидает, что по мере развития моделей они станут более интегрированными в исследовательский процесс, сокращая время на рутинные проверки и позволяя учёным сосредоточиться на глубинных вопросах.

• Упадок малых организаций и локальных сообществ из-за экономических изменений, включая рост двухдоходных семей и снижение волонтерства.
• Консолидация рынков в пользу крупных корпораций, подкрепленная регуляторными рамками и финансовыми стимулами, ограничивающими малый бизнес.
• Технологии и интернет одновременно упростили создание онлайн-сообществ, но также способствовали росту крупных платформ и снижению локальной активности.
• Социальные последствия: потеря чувства общности, статуса в сообществе и роста ощущения изоляции и бессмысленности у индивидуумов.
• Возможности для возрождения малых организаций через низкие барьеры входа в цифровую эпоху и осознание их ценности для общества.

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

Авторы: Коллаборация 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)) прямое вычисление значения считается невозможным из-за его колоссального размера и неразрешимости проблемы остановки в общем случае.