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