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