Великая теорема Ферма — одна из самых знаменитых в истории математики. Она утверждает, что для любого целого n > 2 не существует натуральных чисел x, y и z таких, что xⁿ + yⁿ = zⁿ. Французский математик Пьер Ферма сформулировал ее в 1637 году на полях книги, добавив знаменитую фразу, что нашел «поистине чудесное доказательство», но оно не поместилось на полях. Лишь в 1994 году Эндрю Уайлс и Ричард Тейлор представили строгое доказательство, потребовавшее сотни страниц.
Процесс формализации доказательства на языке Lean означает его перевод с естественного языка на строгий машинный код, который компьютер может проверить пошагово, как программу. Для этого нужно «обучить» компилятор Lean всем предварительным понятиям и известным фактам, которые используются в доказательстве. С 2024 года математики во главе с Кевином Баззардом из Имперского колледжа Лондона ведут проект MathLib — библиотеку формализованной математики, которая должна содержать тысячи страниц предварительных результатов, необходимых для полной формализации доказательства Уайлса и Тейлора. Сроки реализации проекта оцениваются примерно в 10 лет.
Компания Anthropic заявила, что модель «Клод» (Claude) справилась с этой задачей за 11 дней. ИИ сгенерировал код на Lean, содержащий 29 500 промежуточных теорем, и, по утверждению компании, представил полностью верифицируемое доказательство.
Математики единодушно отмечают, что сложность этой задачи на порядок превосходит предыдущие достижения ИИ в формализации — например, в феврале 2026 года нейросеть формализовала доказательство задачи об упаковке шаров в 8 и 24 измерениях, удостоенное Филдсовской премии, но она проще.
Правда, как пишет Nature, есть важный нюанс: код, созданный «Клодом», не является общедоступным и не интегрирован в MathLib. Чтобы использовать его повторно, потребуется колоссальная работа по адаптации. Тем не менее, для самого доказательства это означает переход от 99,9% уверенности к стопроцентной: формальная проверка исключает любые пробелы, которые могли ускользнуть от человеческого глаза даже после десятилетий тщательного анализа.
Математическое сообщество надеется, что ИИ-формализация в сочетании с Lean-верификацией радикально упростит рецензирование статей, которое становится все более трудоемким процессом.
«По мере того как научных статей становится все больше, а сами они — все длиннее и сложнее, процесс рецензирования отнимает больше времени, но при этом его качество снижается, — отметил Фредерик Маннерс, математик из Калифорнийского университета. — Появление у математиков своего рода „волшебной палочки“, способной получить статью с arXiv и либо выдать сертификат, подтверждающий ее корректность, либо указать на ошибку, принесло бы огромную пользу».
Датские и британские математики пришли к выводу, который может разочаровать сторонников демократических выборов: идеально справедливой избирательной системы не существует в принципе. Нельзя одновременно гарантировать, что локальные победы дают локальные места, общее число мест в парламенте точно отражает долю голосов по стране, а размер парламента остается фиксированным.
