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

Anthropic объявила: ИИ-модель Claude «в основном автономно» формализовала Великую теорему Ферма за 11 дней. Результат — 13 млн строк кода на языке Lean и примерно 29 500 промежуточных теорем. Это в пять раз больше, чем вся библиотека формализованной математики Mathlib.

Теорему сформулировал Пьер де Ферма в XVII веке, доказал Эндрю Уайлс лишь в 1995-м — после семи лет тайной работы. Формализация — это перевод доказательства в компьютерный код, чтобы машина могла проверить каждый шаг.

Профессор Кевин Баззард из Имперского колледжа Лондона потратил на это пять лет. Claude справился за 11 дней. По словам Баззарда, доказательство «не опирается ни на что, кроме аксиом математики».

Задачу разбили между ИИ-агентами, которым периодически давали общие указания. Координировать их помог инструмент Prove2Me, первоначально созданный для математиков-людей.

Если такие результаты будут надежно воспроизводиться, ИИ сможет ускорить перевод современной математики в проверяемый вид.

Изображение: Who is Danny/Shutterstock/FOTODOM