Anthropic сообщила, что модель Claude построила проверяемую компьютером версию доказательства Великой теоремы Ферма — гипотезы, которую Пьер Ферма сформулировал в 1637 году, а Эндрю Уайлс доказал в 1995 году на 129 страницах.
Математики рассчитывали, что перевод доказательства Уайлса на язык Lean, понятный компьютеру, займёт несколько лет. Claude справился за 11 дней, действуя почти автономно и опираясь лишь на ограниченный объём высокоуровневых данных.
Модель написала около 13 млн строк Lean-кода — это крупнейший подобный объём за всю историю — и доказала по пути 30 300 промежуточных теорем, 29 500 из которых вошли в финальную версию. Десятки агентов Claude работали параллельно, сгенерировав в сумме около 6 млрд токенов. Первая попытка провалилась, прорыв случился после того, как модели открыли доступ к платформе Prove2Me.
Финальную версию проверил Lean; она опирается только на три стандартные аксиомы системы. Математик Кевин Баззард из Имперского колледжа Лондона, чья работа легла в основу проекта формализации, назвал результат экстраординарным достижением автоформализации и подтвердил корректность доказательства.
Claude не нашёл нового доказательства теоремы — в основу легла упрощённая версия работы Уайлса. Достижение состоит в скорости, с которой ИИ довёл масштабное доказательство до формы, полностью проверяемой компьютером.
