Модель Anthropic за 11 дней формализовала Великую теорему Ферма: 13 млн строк Lean и 29 500 теорем

Заголовок «ИИ доказал теорему Ферма» неточен, и это не придирка: теорему доказал Эндрю Уайлс в 1995 году, а здесь выполнена формализация уже существующего доказательства на языке Lean — именно так называет работу и сама Anthropic. Ценность в другом: эксперты ожидали на такую формализацию годы, корень доказательства сошёлся 18 августа в 02:00 UTC, а результат проверен Lean-чекером на трёх стандартных аксиомах, и независимый comparator подтвердил совпадение формулировки с Mathlib. Кевин Баззард, чьи наработки использовались, оценил результат положительно.

Работали десятки параллельных агентов, и первая серия попыток провалилась — агенты теряли состояние проекта. Прорыв дало подключение Prove2Me Тяньи Пэна и коллег из Columbia University: это не «инструмент оптимизации агентов в длинных процессах», как разошлось по пересказам, а открытая коллаборативная платформа для формализации математики — она держит DAG формулировок теорем, ускоряет компиляцию Lean за счёт разделения формулировок и доказательств по файлам и даёт поиск и переиспользование по описаниям на естественном языке. Автономия тоже была не полной: у Anthropic сказано «largely autonomously», и в тексте приводятся высокоуровневые подсказки человека вроде «Jacobian as a scheme sounds high priority».

Две цифры стоит поправить. Сравнение «29 500 теорем — в пять раз больше главной библиотеки Lean» привязано не к тому показателю: более чем в пять раз Mathlib превышает объём кода (13 млн строк), а не число теорем. А утверждение, будто Anthropic «параллельно срезала цену на чтение кэша на 75%, и кэш-токены составили бо́льшую часть затрат на прогон», — выдумка: на странице про Ферма нет ни слова о ценах и структуре затрат, там сказано лишь, что прогон съел около 6 млрд выходных токенов внутренней исследовательской модели, сопоставимой с Claude Fable 5.1. Продуктовый Claude эту работу не делал.