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

Компания Anthropic сообщила, что ее модель искусственного интеллекта Claude впервые создала полное формальное доказательство Великой теоремы Ферма, которое может быть целиком проверено компьютером. Работа заняла 11 дней: система написала около 13 млн строк кода на языке Lean и доказала десятки тысяч промежуточных утверждений.

Речь не идет о новом доказательстве самой теоремы. Ее сформулировал Пьер Ферма в XVII веке, а окончательное доказательство Эндрю Уайлса было опубликовано в 1995 году. Достижение Claude состоит в том, что известное математическое доказательство было преобразовано в строго формализованную последовательность логических шагов, пригодную для машинной проверки.

Проект возглавил исследователь Anthropic Тяньи Пэн. Для работы использовались десятки агентов Claude, которые распределяли между собой отдельные части задачи и объединяли результаты. По данным компании, система сгенерировала около шести миллиардов выходных токенов.

Полученное доказательство проверил математик Кевин Баззард из Imperial College London, который сам занимается формализацией Великой теоремы Ферма. По его оценке, результат действительно доказывает теорему в рамках стандартных математических аксиом.

Anthropic рассматривает этот эксперимент как свидетельство того, что ИИ уже способен выполнять масштабные проекты по формализации существующей математики.