Как ИИ меняет математику: от решения задач тысячелетия до кризиса верификации

Заголовки в СМИ о том, что искусственный интеллект справился с очередной «задачей тысячелетия» или опроверг давнюю математическую гипотезу, появляются с завидным постоянством. Со стороны бывает непросто разобрать, где здесь исторический научный прецедент, а где — агрессивный маркетинг ИИ-лабораторий. Чтобы сформировать объективную картину, я детально изучил позиции ведущих математиков и исследователей, оценивающих реальное влияние больших языковых моделей на фундаментальную науку. В этом материале разберем, как трансформационные процессы меняют академическую среду, в чём нейросети уже превосходят человека, а где сталкиваются с глухими стенами.

Главное вкратце

За последние годы математические возможности передовых LLM совершили колоссальный скачок. Если ещё недавно алгоритмы пасовали перед школьными текстовыми задачами, то к настоящему моменту крупные ИИ-компании заявляют о решении проблемы Навье — Стокса и подходе к другим фундаментальным проблемам из списка Clay Mathematics Institute.

Из ключевых тенденций стоит выделить следующие аспекты:

• Эпоха изобилия доказательств: Способность моделей генерировать логические выводы растет экспоненциально. Однако, как отмечает лауреат Филдсовской премии Теренс Тао, ценность механического построения доказательств падаёт, а на первый план выходит их понимание, структурирование и верификация.
• Специфика мышления ИИ: Алгоритмы отлично работают «в ширину», сопоставляя концепции из смежных областей, и демонстрируют высокую эффективность в поиске контрпримеров. При этом они пока не способны создавать кардинально новые теоретические базы или совершать концептуальные озарения.
• Бутылочное горлышко верификации: Возросший поток сгенерированных решений (включая ошибочные варианты и так называемый «математический слоп») заставляет ученых активнее внедрять системы формальной верификации, такие как язык Lean.
• Академический кризис и этика: В математическом сообществе растет напряжение: публикуются коллективные манифесты (например, Лейденская декларация), звучат претензии к методам OpenAI и Anthropic, а также формируются новые стандарты публикации научных результатов.

Хронология прорывов: от «стохастического попугая» до задач тысячелетия

Чтобы оценить темпы прогресса, полезно взглянуть на хронологическую цепочку событий последних лет:

• 2022 год: С выходом первых версий ChatGPT преобладало мнение, что языковые модели — это лишь «стохастические попугаи», неспособные к строгой логике и спотыкающиеся об элементарные арифметические условия.
• 2024 год: Появление специализированных reasoning-моделей (начиная с OpenAI o1-preview и заканчивая DeepSeek R1) показало, что обучение с подкреплением (RL) радикально повышает качество решения математических тестов.
• 2025 год: ИИ-системы от OpenAI и Google DeepMind продемонстрировали результаты уровня золотых медалей Международной математической олимпиады. Впрочем, академическое сообщество встретило это сдержанно, указав на разницу между олимпиадными головоломками и реальной исследовательской работой.
• Осень 2025 года: Скепсис усилился, когда заявленные ИИ-доказательства гипотез Эрдёша оказались пересказом уже известных человечеству решений.
• Начало 2026 года: На специализированном ресурсе erdosproblems.com стали появляться первые подлинные решения открытых проблем, пусть и малозначительных.
• Февраль 2026 года: Стартовал академический проект First Proof для независимой оценки способностей нейросетей на свежих задачах. В это же время легендарный Дональд Кнут признал, что Anthropic Opus 4.6 помог ему найти решение проблемы при подготовке очередного тома «Искусства программирования».
• Май — июль 2026 года: OpenAI объявила об опровержении гипотезы Эрдёша о единичном расстоянии, а сотрудник Anthropic опубликовал контрпример к известной проблеме якобиана, найденный моделью Fable прямо во время просмотра футбольного матча.
• Август — сентябрь 2026 года: OpenAI продемонстрировала 10 сложных доказательств, найденных моделью Astra, а Anthropic завершила автоформализацию доказательства Великой теоремы Ферма в Lean. Вскоре OpenAI заявила о получении доказательства для уравнений Навье — Стокса, претендующего на закрытие одной из «задач тысячелетия».

Сильные и слабые стороны больших языковых моделей в науке

Как замечает обладатель Филдсовской премии Тимоти Гауэрс, вопрос не в том, «умнее» ли ИИ человека, а в специфике и характере математического мышления нейросетей.

В чём преимущество нейросетей

• Широта познаний: Человек-математик вынужден глубоко специализироваться в узкой нише. LLM же обучена на всём массиве накопленных человечеством знаний и способна сопоставлять методы из далеких друг от друга разделов математики, находить нестандартные пересечения.
• Меньшая предвзятость: Модели не испытывают пиетета перед авторитетами. Если Пол Эрдёш считал гипотезу верной и все пытались её доказать, модель легко берется за поиск контрпримера и находит его.
• Скорость и комбинаторный перебор: Нейросеть способна перебрать тысячи гипотетических комбинаций за короткое время. Это не просто «грубый брутфорс», а математически оптимизированный поиск решений.
• Неутомимость: Алгоритмы не теряют мотивацию после сотен неудачных попыток. Известны случаи, когда в промптах приходилось в прямом смысле эмоционально подбадривать модель («верь в себя, не сдавайся»), чтобы она продолжала генерацию.
• Обучение в верифицируемых средах: Математика идеально подходит для обучения с подкреплением, так как корректность каждого логического шага можно измерить формальным правилом без необходимости проводить физический эксперимент в реальности.

Скрытые уязвимости и ограничения ИИ

• Уклон в контрпримеры: Алгоритмам намного проще опровергнуть утверждение, подбрав один подходящий объект, чем построить фундаментальное доказательство истинности.
• Дефицит глубины: Большинство сгенерированных решений базируются на комбинировании известных трюков и подходов, а не на создании принципиально новых теорий.
• Низкое качество публикаций: Модели часто выпускают громоздкие, плохо структурированные описания, пропускают важные логические переходы и «забывают» ставить ссылки на предшественников.
• Ошибки и галлюцинации: В тени громких анонсов остаются тысячи сгенерированных ошибочных вариантов и гигантские объемы сожженных вычислительных токенов.
• Финансовая стоимость: Запуск тысяч агентов для решения одной задачи требует миллионных бюджетов, хотя со временем стоимость вычислений непрерывно снижается.

Специфика и текущий стиль работы LLM с математическими задачами

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

Удачная академическая метафора описывает этот процесс так: труды великих ученых — это изолированные горные пики, а доказательства ИИ — поднимающийся уровень воды. Нейросети заполняют «долины» — рутинные, трудоемкие промежуточные задачи, на которые у людей раньше просто не хватало времени и ресурсов.

Lean и концепция формальной верификации

С ростом объёма автоматических вычислений критически выросла роль формальной верификации. Самой популярной средой стал язык Lean и его коллективная библиотека Mathlib.

Проект Lean был создан Леонардо де Мура ещё в 2013 году для проверки софта на баги, но неожиданно стал стандартом среди математиков. Если доказательство записано на Lean, его корректность проверяется машиной автоматически, полностью исключая человеческий фактор и ошибки рецензирования.

Однако Lean не является универсальной панацеей от всех проблем:

• Возможность багов в верификаторе: В самом компиляторе могут кроться ошибки, позволяющие доказать неверные утверждения (проблема «reward hacking»).
• Сложность формализации: Ошибка в исходной формулировке гипотезы приведет к тому, что система формально докажет совершенно другое утверждение.
• Чрезмерный объем кода: Автоматически сгенерированный код Lean может быть невероятно раздут. Например, при формализации доказательства Теоремы Ферма нейросеть Anthropic за 11 дней создала 13 миллионов строк кода. Это доказательство автоматически проверяется, но практически нечитаемо для человека без длительной переработки.

Ситуация в сообществе: «золотая лихорадка», коммерция и академические споры

Массовая засылка открытых проблем в LLM привела к появлению так называемого «математического слопа» — огромного количества необоснованных претензий на прорывы, заполнивших препринты и тематические сайты. Томас Блум, куратор erdosproblems.com, был вынужден ввести строгие правила подачи материалов, требуя от авторов тщательной ручной проверки и раскрытия роли ИИ.

Параллельно обострились конфликты с ИИ-корпорациями. Публикация OpenAI решения проблемы Навье — Стокса вызвала скандал: математик Тристан Бакмастер заявил, что компания могла использовать данные его долгой работы с моделями, задействовав 10 000 агентов одновременно и по сути «подавив проблему железом», опередив автора на финишной прямой.

В ответ на эти вызовы была опубликована Лейденская декларация, призывающая к прозрачности, авторской ответственности за результаты ИИ и соблюдению академической этики.

Перспективы: что ждёт фундаментальную науку дальше?

Эти события подтолкнули сообщество к дискуссии о смысловой цели математики. Популяризатор науки Грант Сандерсон (создатель канала 3Blue1Brown) отмечает, что прогресс ИИ будет оцениваться не бенчмарками, а изменением тональности научных дискуссий.

Математик Дэвид Бессис в своей работе указывает, что наука долгое время находилась в плену «экономики теорем», когда ценность исследователя определялась лишь количеством опубликованных доказательств. На самом же деле, как подчеркивал Уильям Тёрстон, фундаментальная цель математики — это глубокое человеческое понимание и передача знаний. Если ИИ сгенерирует миллионы страниц проверенного Lean-кода, который не способен осмыслить ни один человек, научная ценность такого массива останется под большим вопросом.

Конструктивная модель Теренса Тао: пять этапов жизни доказательства

Теренс Тао предлагает взвешенный взгляд на интеграцию нейросетей. По его мнению, доказательство проходит через пять ключевых фаз:

1. Поиск доказательства: Построение логической цепочки. Здесь ИИ берет на себя рутину, переводя нас в эпоху изобилия результатов.
2. Верификация: Автоматическая проверка с помощью Lean и аналогичных систем.
3. Описание: Создание понятного текста для публикации. На этом этапе человеку пока нет равных, так как модели плохо расставляют смысловые акценты.
4. Принятие сообществом: Коллективное осмысление, дискуссии и оценка важности открытия.
5. Каноникализация: Встраивание результата в учебники, образовательные программы и общенаучный контекст.

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

Источник: habr.com