У математики была репутация последней крепости человеческого разума: нейросети пусть пишут стихи и генерируют видео, но доказать теорему — это, извините, совсем другой уровень абстракции. Крепость сдалась за два года, причём стремительно: системы ИИ вышли на золотой уровень главной школьной олимпиады, помогли закрыть задачу, которую профессионалы годами не могли одолеть, а формально проверяемые доказательства из диковинки превращаются в норму. Что всё это меняет для науки — и для людей, которые ею занимаются, — и попробуем понять.
Первым громким маркером стала Международная математическая олимпиада — главное соревнование школьников планеты, где за четыре с половиной часа надо осилить три задачи, и решают их сильнейшие юные математики мира. В 2024 году AlphaProof от DeepMind вместе с геометрической AlphaGeometry 2 закрыла четыре задачи из шести — уровень серебряной медали. Годом позже о золоте — пяти задачах из шести в полноценном олимпиадном формате — независимо отчитались сразу две лаборатории, Google DeepMind и OpenAI.
Начинка у таких систем гибридная. AlphaProof обучалась с подкреплением прямо в языке Lean: модель предлагает доказательство, формальный проверщик его принимает или бракует — и так миллионы попыток. AlphaGeometry борется с дефицитом данных иначе: порождает себе синтетические чертежи и теоремы и учится на них. Нейросеть угадывает, символический движок считает.
Одна оговорка, и без неё никуда. Олимпиада — спринт с гарантированным ответом: задачи подобраны так, что красивое решение непременно существует и умещается в школьные методы. Исследовательская математика устроена иначе — и самое любопытное сейчас происходит именно там.
Недоверие к машинным доказательствам куда старше нейросетей. Когда в 1976-м компьютер помог осилить проблему четырёх красок, математики потом годами спорили: можно ли считать доказательством перебор, который человек физически не в состоянии проверить? С гипотезой Кеплера вышло ещё показательнее. Рецензенты не смогли вычитать доказательство целиком — и спустя годы команда автора прогнала его через проект Flyspeck, до состояния, когда каждый шаг сверяет программа.
Сегодня символ такой аккуратности — ассистент доказательств Lean и его открытая библиотека mathlib, куда сообщество складывает выверенную математику. Само движение во многом выросло из идей Владимира Воеводского: лауреат Филдсовской премии, математик московского происхождения обнаружил пробел в собственной работе и заключил, что наука так жить не должна. А когда Петер Шольце усомнился, формализуема ли вообще одна из ключевых теорем его теории, энтузиасты за считаные месяцы собрали полное Lean-доказательство — «эксперимент с жидкостными тензорами» стал легендой сообщества.
Для нейросетей формальная проверка — не роскошь, а условие выживания: языковые модели регулярно выдают правдоподобную чушь. Зато уж если доказательство прошло через Lean, оно верно вплоть до аксиом.
Пал Эрдёш оставил после себя сотни открытых задач с назначенными премиями; энтузиасты ведут их онлайн-каталог, где статусы решений обновляются годами. Судя по имеющимся данным, языковые модели уже включились в такую работу: подсказывают, к примеру, какую известную лемму стоит примерить к той или иной конструкции, а людям остаётся довести доказательство и аккуратно всё перепроверить.
Похожих сюжетов множится. FunSearch эволюционным перебором программ улучшила оценки в классической комбинаторной задаче о cap set. Следом AlphaEvolve нашла новую конструкцию для «числа поцелуев» в одиннадцати измерениях — первый прогресс за десятилетия в задаче об упаковке сфер вокруг одной сферы. А ещё раньше SAT-решатель закрыл проблему пифагоровых троек, выдав доказательство объёмом в двести терабайт: прозой такое не прочтёт ни один живой рецензент.
Схема всюду одна. Машина не понимает математику по-человечески — зато гигантски ускоряет перебор гипотез, конструкций и лемм. Вкус и идею пока поставляет человек, грубую силу — кремний.
Роль у России в этой истории двоякая. Олимпиадная школа — одна из сильнейших в мире, и это не комплимент, а констатация: наши школьники регулярно берут золото на международной олимпиаде, а конвейер подготовки отточен десятилетиями — от кружков при университетах до центра «Сириус». Кадровый ресурс для «человеческой» половины гибридной математики огромен. Отсюда, кстати, родом и Воеводский, чьи идеи о проверяемых доказательствах стали мировым мейнстримом.
А вот индустриальная часть цепочки проседает. Яндекс и Сбербанк развивают большие языковые модели (YandexGPT, GigaChat), группы в ВШЭ, МФТИ и Сколтехе работают на стыке машинного обучения и математики, энтузиасты участвуют в мировом сообществе Lean. Но публичных сообщений о российском аналоге AlphaProof — полном цикле от нейросети до верифицированного доказательства — по имеющимся данным, пока не появлялось: такая разработка требует гигантских вычислительных мощностей и долгих вложений в нишевое направление.
Точки входа, впрочем, видны уже сейчас: автоматическая проверка решений в образовании, олимпиадная подготовка, верификация расчётов в инженерных задачах. А сильная математическая школа — главный козырь, если нишу решат развивать всерьёз.
Меняется сама профессия. Математик всё меньше вычислитель и всё больше режиссёр: выбирает задачу, чует, где спрятана красивая структура, формулирует гипотезы, интерпретирует выдачу машины и отвечает за результат. Телескоп ведь не отменил астрономию — он переопределил её масштаб; то же происходит и здесь.
С авторством ясность давно внесена: ведущие научные журналы запрещают указывать ИИ соавтором, а ответственность за текст и корректность лежит на людях. Меняется и доверие: всё ценнее не гладкий текст статьи, а проверяемый артефакт — формализация в Lean, которую каждый может запустить у себя. Отсюда и риск: математика может расколоться на «проверенную» и «правдоподобную», а доступ к сильным моделям превратится в новую форму научного неравенства.
Математика на глазах становится ближе к экспериментальной науке: гипотезы теперь можно клепать сотнями, и ценность смещается от умения «решить» к умению решить осмысленное и доказать безупречно. ИИ пока не заменяет математика — он просто отменяет необходимость быть вычислителем. Автором остаётся человек: тот, кто выбирает вопрос. А вот слово «доказано» окончательно переезжает от рецензента к машине. По-моему, это хорошая новость для обеих сторон.