Claude Fable нашла контрпример к столетней гипотезе Якобиана

Блог Xena Project, площадка одного из мейнтейнеров библиотеки Mathlib для языка формальных доказательств Lean, описывает серию событий конца весны, середины лета 2026 года: за два месяца ИИ-модели несколько раз подряд находили и формально проверяли контрпримеры к математическим гипотезам, которые люди не могли ни доказать, ни опровергнуть десятилетиями.

20 мая 2026 года ChatGPT опроверг гипотезу Эрдёша о единичных расстояниях (задача дискретной геометрии о минимальном числе различных расстояний между точками плоскости), доказательство сводило контрпример к теореме Голода, Шафаревича (теория чисел, 1960-е годы), и его подлинность подтвердили математики, получившие ранний доступ к аргументу. Формализации в Lean на тот момент не было. Через неделю Fields-медалист Майк Фридман, ныне научный директор компании Logical Intelligence (сооснователь, лауреат премии Тьюринга Ян Лекун), сообщил, что их система автоматически формализовала в Lean ключевой шаг статьи ChatGPT, сведение к теореме Голода, Шафаревича; саму 100-страничную теорему теории чисел (для неё нужна глобальная теория полей классов) формализовать тогда не удалось. Ещё через месяц, 26 июня, сотрудник OpenAI Борис Алексеев с помощью новой модели OpenAI Sol получил полную формализацию контрпримера с нуля, не опираясь ни на что, кроме аксиом математики: за три недели модель сгенерировала 1,2 миллиона строк Lean-кода, для сравнения, вся библиотека Mathlib насчитывает 2,3 миллиона строк и писалась девять лет. Автор блога запустил код в песочнице (Lean, полноценный язык программирования, вредоносный код в нём может выполнять произвольные команды) и убедился, что доказательство действительно устанавливает нетривиальные теоремы о когомологиях числовых полей.

В начале июля на семинаре «Formalizing Fermat» (спонсор, Logos Research, разработчик собственного инструмента автоформализации на базе Mathlib, к которому одновременно могли подключаться не более пяти из 25 участников) все посетители получили на месяц бесплатный доступ к OpenAI Sol и модели Anthropic Claude Fable, OpenAI и Anthropic сами предложили подписки, узнав о происходящем. В первый день семинара инструмент Logos нашёл контрпример к одному из утверждений в сгенерированном ИИ конспекте по теории конечных плоских групповых схем, который автор блога готовил для собственного проекта по Великой теореме Ферма, утверждение оказалось ошибочным. Позже профессор Чикагского университета Ахил Мэтью поднял открытый более 60 лет вопрос Гротендика: убивается ли всякая конечная свободная групповая схема порядка n числом n (Делинь доказал это в коммутативном случае, сам Гротендик, для приведённой базы, Рене Схоф и Эмилиано Торти закрыли ещё часть случаев). 11 июля модель Sol нашла контрпример, групповую схему порядка 4, не убиваемую числом 4, а Fable за несколько часов автоформализовала доказательство в файл на 1076 строк Lean-кода; автор блога проверил компиляцию менее чем за пять минут, после чего заявка на включение изменений с контрпримером ушла в Mathlib.

Параллельно в тексте описан быстрый рост использования этих инструментов: аспиранты Имперского колледжа Лондона платят $200 в месяц за доступ к Sol и Fable (один профессор назвал это «сумасшествием», автор блога считает наоборот, не платить эти деньги аспиранту сейчас неразумно), а Гарвардский университет уже даёт бесплатный доступ к Fable всем аспирантам, постдокам и преподавателям. Аспирант автора Эндрю Янг с помощью Sol и Fable написал 250 тысяч строк Lean-кода и по сути завершил формализацию теоремы о поднятии модулярности, ключевого элемента доказательства Великой теоремы Ферма, примерно за две недели.

Финал истории, гипотеза Якобиана, открытая проблема алгебраической геометрии возрастом почти 100 лет: за 12 часов до публикации поста математик Левент Алпёге написал в соцсети X, что модель Fable нашла к ней контрпример, предположительно найденный во время финала чемпионата мира по футболу 2026 года. На момент публикации автор блога сам эту работу не проверял, контрпример вручную формализовал и оформил заявку не в Mathlib (там нет каталога гипотез), а в репозиторий Formal Conjectures от DeepMind, который такой каталог ведёт, математик Пол Лезо.

Автор блога заключает: крупные ИИ-сгенерированные результаты в математике теперь неизбежны, а доверие к ним держится не на тексте модели, а на факте успешной компиляции в Lean. За автоформализацию математики одновременно борются несколько компаний, Logical Intelligence, Logos Research, Harmonic, Axiom AI, Moonshot AI, помимо самих OpenAI и Anthropic.

Ключевые факты

• 20 мая 2026 года ChatGPT опроверг гипотезу Эрдёша о единичных расстояниях; месяц спустя новая модель OpenAI Sol самостоятельно сгенерировала полную формализацию доказательства, 1,2 млн строк кода на Lean за три недели (вся библиотека Mathlib, 2,3 млн строк за девять лет).
• 11 июля модель Sol нашла контрпример к 60-летнему вопросу Гротендика о групповых схемах, модель Claude Fable автоформализовала доказательство за несколько часов; заявка с контрпримером отправлена в библиотеку Mathlib.
• По сообщению математика Левента Алпёге в соцсети X, модель Fable нашла контрпример к гипотезе Якобиана, открытой проблеме алгебраической геометрии возрастом почти 100 лет; математик Пол Лезо вручную формализовал контрпример и отправил его в репозиторий Formal Conjectures от DeepMind.
• За автоформализацию математики на Lean с помощью ИИ параллельно борются несколько компаний: Logical Intelligence (сооснователь, Ян Лекун), Logos Research, Harmonic, Axiom AI, Moonshot AI, а также сами OpenAI и Anthropic.
• Гарвардский университет уже даёт бесплатный доступ к модели Claude Fable всем аспирантам, постдокам и преподавателям; аспиранты Имперского колледжа Лондона платят за такой доступ $200 в месяц.

Почему это важно

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

Кому это важно

Математикам и разработчикам систем формальной верификации, мейнтейнерам Mathlib и Lean; компаниям, строящим инструменты автоформализации (Logical Intelligence, Logos Research, Harmonic, Axiom AI, Moonshot AI, а также OpenAI и Anthropic); университетам, которые уже перестраивают доступ аспирантов и преподавателей к таким моделям, Гарвард выдаёт его бесплатно.

Как это применить

Для проверки ИИ-доказательства математик компилирует сгенерированный Lean-код: если он компилируется без ошибок и опирается только на аксиомы и признанные библиотеки вроде Mathlib, доказательству можно доверять независимо от того, кто его написал. Компании уже предлагают такие инструменты по подписке (около $200 в месяц за модели вроде Sol и Fable) или как отдельный сервис автоформализации, как у Logos Research.

Можно ли доверять

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

Риски и подводные камни

Lean, полноценный язык программирования, и вредоносный сгенерированный код теоретически может выполнять произвольные команды на компьютере того, кто его запускает, поэтому автор блога открывал чужой ИИ-код только в песочнице. Есть и репутационный риск: СМИ путают масштаб разных результатов (например, не отличают контрпример к гипотезе Эрдёша от куда более сложного случая с вопросом Гротендика), а скорость появления контрпримеров к давним гипотезам вызывает у части математиков отрицание, а не признание масштаба сдвига.

«Крупные математические результаты, порождённые ИИ, теперь неизбежны.»

— автор блога Xena Project, мейнтейнер библиотеки Mathlib