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

3 часа назад Прокомментировать Просмотры: 8

Источник изображения: Anthropic

История Великой теоремы Ферма берет свое начало почти четыре столетия назад со скромной заметки Пьера Ферма на полях трактата. Математик утверждал, что диофтово уравнение aⁿ + bⁿ = cⁿ не имеет решений в области целых положительных чисел при показателе n > 2, и даже заявлял, что нашел изящное подтверждение. Правда, свободного места на полях для выкладок катастрофически не хватило. В результате поистине титанический поиск ответа растянулся более чем на три с половиной века.

Эндрю Уайлс презентовал триумфальное доказательство в 1993 году, однако при детальном аудите эксперты выявили уязвимость. На устранение пробела ушел еще почти год, и окончательный вариант научное сообщество увидело лишь в 1995-м. Манускрипт занял 129 страниц и потребовал привлечения колоссального математического аппарата, созданного за столетия после формулировки гипотезы.

Тем не менее, даже верифицированные человеком теоретические выкладки нуждаются в проверке иного уровня. Одним из наиболее надежных стандартов считается формализация — перевод рассуждений на строгий язык, где машина способна проконтролировать каждый дедуктивный шаг. Для этих целей активно применяется интерактивный помощник Lean. Главная сложность заключается в том, что академические тексты пишутся для людей: автор вправе опустить очевидный момент или сослаться на хрестоматийную лемму. Эрудиция же машины требует исчерпывающей детализации логической цепи со всеми промежуточными выводами.

Именно эту титаническую задачу искусственный интеллект Claude решил всего за 11 суток. Масштабная инициатива по формализации теоремы Ферма уже несколько лет координируется научным сообществом под эгидой Кевина Баззарда из Имперского колледжа Лондона, причем завершения проекта ждали еще не один год. Claude практически в автономном режиме преодолел этот рубеж, написав порядка 13 млн строк кода на Lean и попутно доказав 30 300 вспомогательных теорем. В финальный релиз вошли 29 500 из них.

Масштабы сгенерированного кода поражают воображение: результат работы Claude более чем в пять раз превосходит Mathlib — базовый репозиторий формализованных математических теорем, который служил фундаментом. Процесс не сводился к банальному единичному запуску: рой автономных агентов Claude параллельно препарировал абстрактные концепции, выводил отдельные утверждения и стыковал их в монолитную структуру. Совокупный объем генерации составил около 6 миллиардов выходных токенов.

Итоговый массив данных успешно прошел верификацию в системе Lean. В решении задействованы всего три базовые аксиомы среды, а независимый аудит подтвердил полное соответствие формулировки каноническому аналогу из Mathlib. Профессор Баззард, изучив полученные материалы, охарактеризовал проект как беспрецедентный прорыв в сфере автоформализации и официально подтвердил безупречность логики.

Стоит уточнить, что Claude не открыл принципиально новый путь к разгадке теоремы Ферма — в основу легла адаптированная и упрощенная версия наработок Уайлса. Главная ценность эксперимента в другом: ИИ впервые в истории сумел за считанные дни довести доказательство колоссальной сложности до вида, полностью верифицируемого кремниевым разумом.

Для фундаментальной науки это достижение способно стать переломным моментом, затмевающим даже чистую скорость вычислений. Ручной аудит свежих теоретических работ нередко затягивается на месяцы и годы, а с внедрением нейросетей объем математического контента лавинообразно возрастет. Автоматизированная формализация позволит взять трудоемкую проверку на себя, предоставив ученым инструмент для мгновенной детекции логических сбоев в гигантских массивах данных.