Мы делимся первым полным компьютерно-проверенным доказательством Великой теоремы Ферма. Claude работал в значительной степени автономно в течение 11 дней, чтобы написать доказательство на языке программирования Lean. Ниже мы описываем, как была выполнена формализация, и делимся некоторыми мыслями о том, что эта работа может означать для исследовательской математики.

Около 1637 года Пьер де Ферма записал утверждение на полях своего экземпляра «Арифметики» Диофанта, которое стало одной из самых известных математических гипотез всех времен: не существует положительных целых чисел a, b, c, удовлетворяющих aⁿ + bⁿ = cⁿ для любого n > 2. Великая теорема Ферма (ВТФ), как стала известна гипотеза, оказалась невероятно сложной для доказательства. Первое доказательство, представленное сэром Эндрю Уайлсом в 1995 году, состояло из 129 страниц и потребовало месяцев кропотливой работы для проверки.

Десять лет спустя голландский компьютерный ученый Ян Бергстра предложил «формализовать» доказательство Уайлса: преобразовать математические рассуждения в форму, которую компьютеры могут проверять автоматически. С тех пор математики разрабатывают методы, необходимые для кодирования такого сложного доказательства, включая многолетние усилия сообщества, начатые в 2024 году Кевином Баззардом в Имперском колледже Лондона для завершения формализации с использованием ассистента доказательств Lean.

Недавно Тяньи Пэн, исследователь Anthropic, чья группа в Колумбийском университете создает инструменты для формализации с помощью ИИ, решил проверить, сможет ли Claude продвинуться в формализации ВТФ. Результат превзошел его ожидания. За 11 дней, работая в значительной степени автономно, Claude создал первое сквозное компьютерно-проверенное доказательство ВТФ. По ходу работы он написал 13 миллионов строк кода на Lean и доказал 29 500 промежуточных теорем.