ИИ впервые помог формально верифицировать доказательства лауреата Филдсовской премии
Доказательства Марины Вязовской, получившей Филдсовскую премию за решение задачи упаковки сфер в 8 и 24 измерениях, впервые формально верифицированы компьютером
В математике существует особый вид признания, который стоит выше любых наград: когда компьютер подтверждает, что ваше доказательство абсолютно безупречно. Доказательства украинского математика Марины Вязовской, принесшие ей Филдсовскую премию в 2022 году, только что прошли именно такую проверку — и сделали это при беспрецедентном участии искусственного интеллекта.
Вязовская получила свою медаль за решение одной из самых элегантных и коварных задач в математике — задачи упаковки сфер. Звучит просто: как наиболее плотно расположить одинаковые шары в пространстве? В двух измерениях ответ знает каждый пчеловод — это соты. В трёх измерениях оптимальна пирамида из шаров, знакомая любому, кто видел стопку апельсинов на прилавке. Но с ростом числа измерений задача становится чудовищно сложной. В 2016 году Вязовская доказала, что симметричная структура E8 — лучшая упаковка в восьмимерном пространстве, а вскоре совместно с коллегами установила, что решётка Лича оптимальна в 24 измерениях. При всей кажущейся абстрактности эти результаты имеют прямое отношение к кодам с коррекцией ошибок, которые используют смартфоны и космические зонды.
Математическое сообщество проверило и признало доказательства верными — отсюда и Филдсовская премия. Однако формальная верификация — процесс, при котором каждый логический шаг доказательства проверяется компьютерной программой, — задача принципиально иного масштаба. Человеческий рецензент может пропустить тонкую ошибку, компьютер — нет. Именно поэтому формализация сложных доказательств считается «золотым стандартом» достоверности в современной математике.
Всё началось со случайной встречи. В Лозанне студент третьего курса Сидхарт Харихаран рассказал Вязовской, как использует формализацию доказательств в языке Lean для глубокого понимания математических концепций. Lean — это одновременно язык программирования и так называемый «помощник доказательств», позволяющий записывать математические рассуждения в форме, которую компьютер способен проверить на абсолютную корректность. Вязовская заинтересовалась, и в марте 2024 года родился проект Formalising Sphere Packing in Lean. К нему присоединились эксперты из Имперского колледжа Лондона, Университета Восточной Англии и Калифорнийского университета в Беркли. Команда создавала «чертёж» — человекочитаемую карту всех элементов восьмимерного доказательства, отмечая, какие из них уже формализованы, а какие ещё предстоит перевести на язык Lean.
Два года кропотливой работы — а затем произошёл перелом. В октябре 2025 года к проекту подключился стартап Math, Inc., разработавший ИИ-систему Gauss. Это не обычная языковая модель: Gauss представляет собой «рассуждающего агента», способного чередовать естественноязыковые рассуждения с полностью формализованным математическим выводом. Фактически это ИИ, который умеет автоматически переводить математические доказательства на язык, понятный компьютерному верификатору. Подключение Gauss радикально ускорило процесс формализации, позволив завершить то, что иначе заняло бы ещё годы ручной работы.
Результат вызвал серьёзный резонанс в научном сообществе. «Эти новые результаты выглядят очень и очень впечатляюще и определённо сигнализируют о быстром прогрессе в этом направлении», — отметил Лиам Фаул, постдок Принстонского университета и эксперт по ИИ-рассуждениям, не участвовавший в проекте. По его словам, формальная верификация — это своего рода «печать качества», абсолютная гарантия того, что каждый шаг логических рассуждений корректен.
Значение этого прорыва выходит далеко за рамки одного доказательства. До недавнего времени формализация серьёзных математических результатов была настолько трудоёмким процессом, что за неё брались лишь единичные проекты. Если ИИ-системы вроде Gauss смогут систематически ускорять эту работу, математика получит нечто беспрецедентное: возможность массовой верификации доказательств, накопленных за десятилетия. Это не замена математиков — Вязовская по-прежнему совершила интеллектуальный подвиг, которого машина не способна повторить. Но ИИ оказывается незаменимым в самой рутинной и ответственной части работы — проверке того, что гениальная интуиция не привела к ошибке на каком-то из тысяч логических шагов.
Мы наблюдаем рождение новой модели сотрудничества: человек формулирует идеи и строит доказательства, а машина гарантирует их безупречность. Для математики, где одна незамеченная ошибка может поставить под сомнение десятилетия последующих исследований, это не просто удобство — это смена парадигмы.