ИИ впервые полностью формализовал доказательство Великой теоремы Ферма — и компьютер его проверил

Формальное доказательство — это доказательство, записанное так, что каждый шаг проверяет программа, а не рецензент. Ошибиться тут невозможно: если проверка прошла, теорема доказана исходя только из аксиом математики.

Задача — получить полное проверенное машиной доказательство теоремы: для n ≥ 3 не существует натуральных a, b, c, при которых aⁿ + bⁿ = cⁿ.

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

Опорой стали материалы проекта Баззарда и библиотека Mathlib. Формализация следует упрощённому изложению доказательства Дармона, Даймонда и Тейлора.

Судья один — программа проверки Lean. Результат дополнительно перепроверили двумя независимыми средствами.

11 дней, 13 миллионов строк. Доказательство на Lean более чем в 5 раз больше всей библиотеки Mathlib.

29 511 теорем в итоговом доказательстве. На это ушло около шести миллиардов выходных токенов внутренней исследовательской модели.

Без пропусков. Проект собирается без единого «sorry» — места, оставленного недоказанным, — и опирается только на три стандартные аксиомы.

Код открыт под лицензией Apache 2.0: github.com/anthropics/fermats-last-theorem.

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