Anthropic 4 сентября сообщила, что агенты Claude за 11 дней подготовили первую полностью проверенную компьютером версию доказательства Великой теоремы Ферма. В объявлении указано, что работа была завершена в прошлом месяце. Компания подчёркивает, что это именно формализованное доказательство, прошедшее машинную верификацию от начала до конца.

Что произошло

По словам Anthropic, команда использовала подход формализации — перевода математических рассуждений в строгий вид, который могут проверять компьютерные ассистенты доказательств, такие как Lean. Результат описан как «первая» полностью проверенная компьютером версия доказательства по этой задаче. Срок выполнения — 11 дней — заявлен для агентов Claude.

Зачем нужна формализация

Проверка больших математических доказательств человеком может занимать годы. Формализация помогает ускорить и обезопасить этот процесс, поскольку вычислительная система последовательно проверяет каждый шаг рассуждений в рамках заданной логики и аксиом. Anthropic указывает именно на ценность такого подхода для надёжной верификации крупных результатов.

Контекст

Великая теорема Ферма — классическая задача теории чисел, вокруг которой столетиями шли исследования. В популярной формулировке она связана с уравнением aⁿ + bⁿ = cⁿ. В сообщении Anthropic речь идёт не о новом математическом открытии, а о первом полном прохождении компьютерной проверки формализованного доказательства.

Даты и детали

Anthropic сделала объявление 4 сентября 2026 года, отметив, что завершение формализации состоялось в прошлом месяце. Заявленный срок подготовки формализованной версии доказательства агентами Claude — 11 дней.