➗ Claude впервые формализовал великую теорему Ферма в Lean

Anthropic сообщила, что её ИИ-модель Claude практически автономно за 11 дней создала первую полностью проверяемую компьютером формализацию великой теоремы Ферма. Результат записан на языке Lean — всего Claude написал 13 миллионов строк кода и доказал 29 500 промежуточных теорем. Готовое доказательство опубликовано на GitHub.

Формализация переводит математическое рассуждение в вид, который компьютер может проверить автоматически, без опоры на «очевидные» шаги, пропускаемые в человеческих доказательствах. Оригинальное доказательство Эндрю Уайлса 1995 года занимало 129 страниц, а его проверка заняла месяцы. Сообщество математиков ожидало, что формализация такой сложной теоремы займёт годы — один лишь «чертёж» проекта насчитывал 86 страниц. Claude справился за полторы недели, а профессор Кевин Баззард, лидер сообщества по формализации FLT, назвал результат экстраординарным и пригодным для дальнейшего построения.

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

#AI #Claude #Lean #Math #Formalisation