ПУАНКАРЕ, ПРОВЕРЕННЫЙ МАШИНОЙ СТРОКА ЗА СТРОКОЙ

Проверка доказательства — одна из самых трудоёмких задач в математике, особенно когда рассуждение охватывает несколько областей. По мере того как ИИ ускоряет производство доказательств, надёжная проверка становится важнее. Системы автоматической проверки доказательств (proof assistants), такие как Lean 4, предлагают один из ответов: определения, утверждения и доказательства записываются как код, а небольшое доверенное ядро программы, её «kernel», проверяет каждый шаг. Доказательство, прошедшее ядро, устанавливает своё утверждение; людям остаётся проверить, что утверждение действительно говорит то, что имеют в виду математики.

Сжатое доказательство и недостающая библиотека

Гипотеза Пуанкаре, доказанная Перельманом, утверждает, что всякое замкнутое односвязное трёхмерное многообразие — неформально, конечное трёхмерное пространство без дыр, за которые могла бы зацепиться петля, — эквивалентно трёхмерной сфере. Доказательство следует программе потока Риччи, начатой Ричардом Гамильтоном. Три препринта Перельмана 2002–2003 годов излагали ключевые аргументы в крайне сжатой форме; подробные изложения появились позже, в том числе монография Джона Моргана и Ган Тяня 2007 года, которой и следует этот проект.

Доказательство опирается на геометрический анализ, которого в общей библиотеке Lean, Mathlib, по большей части не было. Значительную часть основ пришлось строить с нуля.

Вехи, замороженные математиками

Чжиюань Чжан, Аксель Делаваль, Бинь Дун, Чуньлэй Лю и коллеги из Пекинского университета и других пекинских институтов начали работу в мае 2026 года: три «ИИ-инженера» с математической подготовкой работали вместе с математиками. Их первый подход — формализовать крупные блоки фоновой теории — оказался медленным, а полученный код не оправдал ожиданий.

В сентябре 2026 года они начали заново. Доказательство разрезали примерно на 90 вех, каждая из которых — точное утверждение на Lean с нужными ему определениями. Математики проверяли эти утверждения до или во время их формализации, после чего утверждения замораживались: агенты не могли их менять, а любые исправления возвращались к математикам. Поскольку никто не мог прочитать каждую строку, написанную агентами, эти вехи стали контрольными точками, где люди проверяли математику.

Затем агенты работали параллельно — через интерактивные сессии с инструментами программирования, в основном Codex и Claude Code, и через систему Archon Horizon, которая рассылает ограниченные «миссии» на множество серверов. Бот компилировал каждый вклад и сливал принятые. Основную часть формализации утверждений и построения доказательств выполнила GPT-6-Astra; Fable-5.1 использовалась для независимых проверок, диагностики застрявших задач и проверки утверждений.

2,8 миллиона строк примерно за две недели

После месяцев подготовки основная формализация заняла чуть больше двух недель. Подписки на ИИ и аренда серверов обошлись примерно в 25 000 долларов. Разработка доказывает и топологическую, и гладкую версии теоремы, полностью компилируется и проходит независимую проверку по целевым утверждениям, записанным только средствами Mathlib.

Объём огромен: около 3,2 миллиона строк на Lean, сокращённых до 2,8 миллиона, если оставить лишь то, от чего зависит итоговая теорема. По подсчётам авторов, почти половина — фоновая теория. Один классический результат, который Морган и Тянь упоминают в единственной сноске, — о гладких структурах на трёхмерных многообразиях — потребовал сам по себе около 650 000 строк.

Что всё же делали люди

Авторы делят препятствия на три вида: математические пробелы, проблемы реализации на Lean и проблемы координации. Люди задавали рамки утверждений (например, когда ограничить результат тремя измерениями), находили недостающие аргументы — такие как шаг локальной компактности, который агенты не могли найти, — и выявляли скрытые допущения. Их главный вывод: организация работы значила не меньше, чем возможности агентов. Тот же вывод они делают из недавней формализации Великой теоремы Ферма компанией Anthropic, которой тоже пришлось начинать заново после того, как первые попытки потеряли нить состояния проекта.

Проверено, но ещё не прибрано

Авторы не считают работу законченной. Код полон дублирования; доказательства агентов не всегда следуют эталонному пути; а превратить всё это в переиспользуемую библиотеку геометрического анализа — следующая задача. Объявлено и о независимой формализации той же гипотезы другой командой. Их надежда: однажды один математик сможет с помощью таких инструментов проверять собственные исследования.

Конфликт интересов. Команда использовала Claude Code и модель Fable-5.1, обе от Anthropic, наряду с GPT-6-Astra, доступной через подписки OpenAI, которая выполнила большую часть работы. В статье проект также сравнивается с формализацией Великой теоремы Ферма компанией Anthropic. Этот текст написан Claude.