Anthropic сообщила, что агенты Claude за 11 дней формализовали доказательство теоремы Ферма в системе Lean. Для этого было сгенерировано 13 млн строк кода и 30 300 промежуточных теорем, из которых в финальное доказательство вошли 29 500. Результат проверил компилятор Lean и подтвердил математик Кевин Баззард, ведущий проект формализации этой теоремы с 2024 года. Процесс не был полностью автономным, но человек лишь изредка давал указания верхнего уровня. Anthropic сообщила, что агенты Claude за 11 дней формализовали доказательство теоремы Ферма в системе Lean. За основу взята упрощённая версия доказательства Уайлса от Дармона, Даймонда и Тейлора. Сгенерировано 13 млн строк кода и 30 300 промежуточных теорем, из которых в финальное доказательство вошли 29 500. Результат проверил компилятор Lean и подтвердил математик Кевин Баззард, ведущий проект формализации этой теоремы с 2024 года. Первые попытки проваливались. Агенты теряли состояние проекта и переставали координироваться, их неудачные заходы дали около 7% строк итогового кода. Сработало после перехода на платформу Prove2Me, которая держит граф теорем и позволяет агентам работать параллельно, смягчая деградацию памяти на длинной дистанции. Это показывает, что для сложных математических задач важна не только мощность модели, но и инфраструктура, которая поддерживает длительное выполнение и координацию нескольких агентов. Полностью автономным процесс не был — человек изредка давал указания верхнего уровня. Смысл автоматизации в том, что люди-рецензенты уже не успевают проверять поток доказательств, а формализация снимает с них часть нагрузки. Результат не представляет новой математики — само доказательство принадлежит Эндрю Уайлсу 1995 года. Но формализация в Lean позволяет проверить его механически, без опоры на человеческое суждение, что важно для доверия к сложным доказательствам в будущем.