Anthropic: Claude за 11 дней написал Lean-доказательство теоремы Ферма

Anthropic опубликовала полное доказательство Великой теоремы Ферма на Lean 4: 13 млн строк, 29 500 промежуточных теорем и около 6 млрд выходных токенов, созданных агентами Claude за 11 дней. Математик Кевин Баззард подтвердил корректность, но отметил, что математической ценности работа не несёт.

• 13 млн строк Lean — более чем в пять раз больше всей библиотеки Mathlib
• Сборка с нуля заняла 5 ч 32 мин на 96 потоках, пик памяти 153 ГБ
• Независимое ядро nanoda проверило 1 052 234 декларации без ошибок
• Оценка стоимости токенов по прайс-листу — около $300 000