Claude формализовал доказательство Великой теоремы Ферма за 11 дней
История Великой теоремы Ферма началась почти 400 лет назад с короткой записи Пьера Ферма на полях книги. Математик утверждал, что уравнение aⁿ + bⁿ = cⁿ не имеет решений в положительных целых числах при n > 2, и уверял, что знает доказательство. Однако места на полях для него, по собственным словам Ферма, не хватило. В итоге поиск решения растянулся более чем на 350 лет.
То, на что математики рассчитывали потратить годы, Claude сделал практически автономно: написал 13 млн строк кода и доказал 29 500 промежуточных теорем
Эндрю Уайлс представил доказательство в 1993 году, но при его проверке обнаружился пробел. На исправление ушёл ещё примерно год, и окончательный вариант появился в 1995 году. Доказательство заняло 129 страниц и использовало сложнейшие математические конструкции, накопленные за столетия после того, как Ферма сформулировал свою теорему.
Но даже доказанное человеком утверждение можно проверять по-разному. Один из самых надёжных способов — формализовать доказательство, то есть перевести его на язык, в котором компьютер способен проверить каждый логический переход. Для этого часто используют Lean. Проблема здесь состоит в том, что математический текст рассчитан на человека: автор может пропустить очевидный шаг или сослаться на известную лемму. Компьютеру же необходимо явно предоставить всю цепочку рассуждений, включая используемые промежуточные результаты.
Источник изображения: Anthropic
Именно эту работу Claude выполнил за 11 дней. Проект по формализации Великой теоремы Ферма уже несколько лет развивает математическое сообщество во главе с Кевином Баззардом из Имперского колледжа Лондона, причём завершение всей работы ожидалось лишь через несколько лет. Claude практически автономно прошёл этот путь, создав около 13 млн строк Lean-кода и доказав «по дороге» 30 300 промежуточных теорем. В финальную версию вошли 29 500 из них.
Масштаб получившегося кода тоже впечатляет: доказательство Claude более чем в 5 раз объёмнее Mathlib — основной библиотеки формализованных математических доказательств, на которую оно опирается. При этом работа не сводилась к одному длинному запуску: десятки агентов Claude параллельно разбирали математические понятия, доказывали отдельные утверждения и собирали их в единую цепочку. Всего на проект ушло около 6 млрд выходных токенов.
Финальную версию проверил Lean. Она использует только 3 стандартные аксиомы системы, а отдельная проверка подтвердила, что формулировка теоремы соответствует её версии в Mathlib. Баззард, ознакомившись с результатом, назвал работу экстраординарным достижением автоформализации и подтвердил корректность доказательства.
При этом Claude не нашёл нового доказательства Великой теоремы Ферма: в основу легла упрощённая версия доказательства Уайлса. Главное достижение здесь в другом — ИИ впервые смог за считанные дни довести настолько масштабное математическое доказательство до полностью проверяемой компьютером формы.
Для современной математики это может оказаться не менее важным, чем скорость конкретного проекта. Проверка новых доказательств людьми иногда занимает месяцы и годы, а с распространением ИИ математических результатов станет больше. Автоматическая формализация может взять на себя значительную часть этой проверки и дать математикам способ быстро установить, не содержит ли огромная логическая конструкция ошибок.
ИИ уже пишет научные статьи, а в Nature поднимают вопрос: кто теперь автор, а кто — просто «сделал полезный комментарий»?