ИИ-система Claude, разработанная компанией Anthropic, подготовила первую полностью проверенную компьютером версию доказательства Великой теоремы Ферма всего за 11 дней. Об этом стало известно 4 сентября 2026 года. Доказательство состоит из 13 миллионов строк кода, что делает его крупнейшим доказательством, когда-либо созданным на платформе Lean, способной проверять математические доказательства. Великая теорема Ферма, высказанная еще в 1637 году, утверждает, что нет трех положительных целых чисел a, b и c, которые бы удовлетворяли уравнению aⁿ + bⁿ = cⁿ для любого значения n больше 2.
Проект, занимающийся формализацией доказательства теоремы Ферма, был запущен в 2024 году математиком Кевином Баззардом в Имперском колледже Лондона. В отличие от Claude, работа его команды не принесла результатов до сих пор. Баззард подтвердил, что доказательство Claude соответствует основным аксиомам математики, и добавил, что такое формализация помогает верифицировать научные статьи и выявлять недочеты в математических рассуждениях. Система использовала библиотеку Mathlib и методику с множеством агентов, работающих параллельно, что помогло эффективно организовать процесс выработки доказательства.
Значение достижения Claude в том, что оно предлагает новый подход к верификации математических доказательств. Ожидается, что эта работа позволит значительно ускорить процесс проверки и позволит математикам более эффективно справляться с задачами формализации, которые в настоящее время требуют большого объема времени и ресурсов. Полный код уже опубликован на GitHub, что позволяет другим исследователям ознакомиться с результатами работы и верифицировать их самостоятельно. Баззард продолжит свой проект по формализации, таким образом обогащая инструменты для проверки математических аргументов в научных исследованиях.