По словам Anthropic, её ИИ Claude создал первое полностью проверенное компьютером доказательство Великой теоремы Ферма, выполнив работу в основном самостоятельно за 11 дней и написав самое длинное математическое доказательство в истории.

Проект под руководством людей в Имперском колледже Лондона работает над той же задачей с 2024 года и далёк от завершения. Claude опередил его на финише. Кевин Баззард, математик, возглавляющий проект в Имперском колледже, проверил доказательство Claude и подтвердил, что оно выдерживает проверку, опираясь исключительно на базовые логические правила математики.

По данным Anthropic, Claude написал самое длинное математическое доказательство в истории и использовал его для формального доказательства Великой теоремы Ферма — задачи, оставлявшей математиков в недоумении 358 лет. ИИ справился за 11 дней, в основном самостоятельно, создав 13 миллионов строк кода, которые компьютер может проверить построчно, вместо того чтобы полагаться на слово математика.

Великая теорема Ферма утверждает, что не существует трёх положительных целых чисел, каждое из которых возведено в степень выше 2, таких, что сумма первых двух равна третьему. Пьер де Ферма записал это утверждение на полях математической книги в 1637 году, добавив, что у него есть «поистине чудесное доказательство», которое не помещается на полях. Затем он умер. Следующие 358 лет математики пытались восстановить то, что он, по его мнению, придумал.

Доказать и проверить — две разные задачи

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

Формализация доказательства означает перевод его на язык настолько буквальный, что компьютер может самостоятельно проверить каждый шаг, не прибегая к субъективным оценкам.

Математики давно испытывают трудности с проверкой. Немецкая премия 1908 года — стоимостью примерно от 1 до 2 миллионов долларов по нынешним деньгам, назначенная за первое верное доказательство теоремы, — уже в первый год получила 621 ошибочную работу.

Как написал Anthropic в X:

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

Настоящее доказательство появилось лишь в 1995 году благодаря британскому математику Эндрю Уайлсу, и с ним связан неожиданный поворот. Уайлс объявил о своём решении в ходе трёх лекций в июне 1993 года, но позже рецензент обнаружил в нём пробел. Почти год он исправлял его вместе с бывшим студентом Ричардом Тейлором, был на грани отказа и наконец опубликовал исправленное доказательство объёмом 129 страниц в мае 1995 года. Оно опиралось на математику, которой не существовало во времена Ферма, — это одна из главных причин, почему математики теперь сомневаются, что собственное «чудесное доказательство» Ферма вообще работало.

Компьютерно-верифицированная математика сама по себе существует уже десятилетия. Первым знаменитым случаем стало компьютерное доказательство теоремы о четырёх красках 1976 года, которое породило продолжающиеся споры о том, следует ли считать доказательством то, что ни один человек не может полностью прочитать вручную. Формальные языки доказательств вроде Lean — созданные Леонардо де Мурой, изначально в Microsoft Research, — выросли именно из этого противоречия: программное обеспечение выполняет проверку, чтобы люди могли доверять результату.

В 2024 году математик Имперского колледжа Лондона Кевин Баззард запустил проект, чтобы сделать именно то, что только что сделал Claude: перевести доказательство Уайлса на Lean — язык, который могут проверять компьютеры. Это работа, требующая армии математиков-волонтёров: собственный план проекта занимает 86 страниц, а его финансирование обеспечено до 2029 года. Claude выполнил всю работу за 11 дней.

Как Claude на самом деле это сделал

Anthropic объясняет в более подробном материале, что Тяньи Пэн, разрабатывающий инструменты ИИ-формализации со своей командой в Колумбийском университете, решил проверить, как далеко Claude сможет продвинуться самостоятельно. Десятки агентов Claude работали параллельно, записывая определения, доказывая небольшие результаты и складывая их в более крупные, практически без участия человека — лишь с редкими подсказками вроде «сначала докажи эту теорему».

Поначалу всё шло не гладко. На раннем этапе агенты постоянно теряли представление о том, что уже доказано, и переставали сотрудничать; эти ложные начала по-прежнему составляют около 7% строк в итоговом доказательстве.

Проблему решил инструмент под названием Prove2Me, также созданный командой Пэна: он давал каждому агенту один и тот же актуальный список задач — какие более мелкие доказательства ещё нужно выполнить, — чтобы никто не дублировал работу и не отклонялся от курса. Он также организовывал файлы так, чтобы Lean проверял всё быстрее, и вёл заметки простым английским о каждом результате, чтобы агенты могли использовать работу друг друга, а не начинать заново.

К концу работы Claude доказал более 30 000 вспомогательных теорем и израсходовал миллиарды токенов, работая на исследовательской модели, которая, по словам Anthropic, примерно соответствует Claude Fable 5.1 — версии, позже выпущенной для широкой публики. Итоговое доказательство занимает 13 миллионов строк — более чем в пять раз больше Mathlib, общей библиотеки, которой математики уже пользуются для подобных задач.

Типичный роман содержит около 80 000 слов. Доказательство Claude эквивалентно 160 романам чистой логической аргументации.

Так имеет ли это вообще значение?

Баззард — чья собственная версия этого проекта остаётся профинансированной до 2029 года — проверил доказательство Claude и дал ему своё одобрение, заявив, что оно доказывает теорему «без каких-либо допущений, кроме аксиом математики».

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

Это не новая проблема. Компьютерное доказательство гипотезы Кеплера заняло четыре года, прежде чем экспертная панель согласилась лишь на оценку «99% уверенности», а доказательству Григория Перельмана гипотезы Пуанкаре потребовалось примерно столько же времени, чтобы полностью получить признание.

Тем, кто не хочет верить Anthropic на слово, этого и не требуется. Полное доказательство объёмом 13 миллионов строк находится на GitHub, доступное бесплатно любому математику с достаточным количеством свободного времени, чтобы разобрать его построчно.