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

Теорема была доказана в 90-х британским математиком Эндрю Уайлсом. Сейчас Claude дали доказательство, а он разложил его на тысячи промежуточных утверждений и записал всё это на языке Lean. После этого компьютер автоматически проверил, что каждый шаг логически корректен.

Claude работал в основном автономно командой из десятков агентов. Агенты написали около 13 миллионов строк Lean и доказали 29.5 тысяч промежуточных теорем. Люди давали лишь редкие подсказки.

Формализация современной сложной математики раньше считалась работой на годы. Claude выполнил задачу за 11 дней. На проект ушло около 6 миллиардов выходных токенов модели, сопоставимой по уровню с Fable 5.1.

https://www.anthropic.com/research/formalizing-fermats-last-theorem