Claude за 11 дней завершил формализацию Великой теоремы Ферма

Агенты Claude за рекордные 11 дней подготовили первую полностью компьютеризированную версию доказательства Великой теоремы Ферма. О достижении 4 сентября сообщила компания Anthropic. Данная формализация опирается на известное доказательство, предложенное Эндрю Уайлсом в 1995 году, и переведена в код, который проверяет система Lean.

Великая теорема Ферма, сформулированная в 1637 году, утверждает, что для положительных целых чисел a, b и c равенство aⁿ + bⁿ = cⁿ невозможно при целых n, превышающих два. Claude успешно перевел математические рассуждения в код, который проверяется шаг за шагом.

Проект возглавил исследователь из Anthropic Тяньи Пэн. Его команда в Колумбийском университете работает над формализацией математики. В процессе эксперимента агенты Claude самостоятельно создавали и проверяли промежуточные утверждения, используя библиотеку Mathlib и ресурсы проектов Imperial College London FLT.

Координация работы агентов осуществлялась через платформу Prove2Me, которая разбивает задачу на части и позволяет нескольким агентам работать одновременно. В результате было доказано около 30 300 промежуточных теорем, из которых 29 500 вошли в итоговый код объемом 13 млн строк.

Anthropic заявила, что это крупнейшее доказательство, выполненное с использованием Lean. Полный код и инструкции доступны на GitHub, где подтверждается его проверка системой Lean и независимым ядром nanoda. Также выяснено, что доказательство опирается на три стандартные аксиомы Lean.

Математик Кевин Баззард из Имперского колледжа Лондона подтвердил результат в своем блоге, подчеркивая значимость автоматической формализации. Он продолжит работу над собственным проектом, нацеленным на пополнение Mathlib и создание доступной документации по доказательству.