200 лет ожидания и одна бессонная ночь. ИИ нашел связь между современной геометрией и формулами XIX века.

Пять лет назад математики Давэй Чэнь и Квентен Жандрон работали над сложной задачей из алгебраической геометрии, связанной с дифференциалами, то есть инструментами анализа, которые помогают измерять «расстояния» вдоль искривленных поверхностей. В какой-то момент их рассуждение уперлось в неожиданную проблему: ключевой шаг опирался на необычную формулу из теории чисел, но исследователи не смогли ни доказать ее, ни аккуратно обосновать. В итоге результат пришлось оформить как гипотезу, а не как теорему.

Недавно Чэнь попытался вернуться к этой задаче с помощью ChatGPT, часами подбирая запросы в надежде получить рабочее доказательство, но заметного прогресса не было. Перелом случился на конференции по математике в Вашингтоне: на приеме Чэнь встретил Кена Оно, известного математика, который недавно ушел из Университета Вирджинии и присоединился к стартапу Axiom. Компания разрабатывает ИИ-инструменты для доказательства теорем, а одним из ее сооснователей стала Карина Хонг, бывшая ученица Оно.

Чэнь рассказал Оно о своей нерешенной проблеме, и уже на следующее утро получил готовое доказательство, которое сгенерировала система AxiomProver. По словам Чэня, после этого «все естественно встало на свои места». Вместе с командой Axiom он оформил материал в статью, и теперь она опубликована на arXiv.

Как описывает Axiom, их инструмент нашел связь между задачей Чэня и Жандрона и числовым явлением, которое впервые изучали еще в XIX веке. Затем система построила доказательство и, что особенно важно для математики, самостоятельно проверила его корректность. Оно утверждает, что ИИ заметил то, что упустили люди.

В Axiom говорят, что это не единичный случай: за последние недели их система предложила несколько новых доказательств для задач, которые годами оставались трудными для специалистов в разных областях. Речь пока не о самых знаменитых и «дорогих» математических проблемах, но о вопросах, которые реально тормозили продвижение в конкретных направлениях. На этом фоне все больше математиков начинают использовать ИИ-инструменты не только для поиска идей, но и для доведения рассуждений до строгих, проверяемых доказательств.

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

Подход Axiom строится на сочетании больших языковых моделей и собственной системы рассуждения AxiomProver, заточенной под получение доказательств, которые можно формально проверить. Для этого используется Lean, специализированный математический язык и экосистема для верификации. В компании подчеркивают, что такой контур отличает их инструмент от «обычных» моделей: он не только генерирует текст, но и обязан пройти проверку в формальном представлении, что снижает риск красивых, но неверных рассуждений. В 2024 году Google показала похожую идею с AlphaProof, а Хонг утверждает, что в их системе применены более новые техники и заметные улучшения.

Помимо истории с гипотезой Чэня и Жандрона, Axiom приводит и другие примеры. Один из них связан с гипотезой Фела о синергиях (syzygies), то есть о конструкциях в алгебре, где соотношения между выражениями «выстраиваются» определенным образом. Примечательно, что в этой теме фигурируют формулы, найденные более 100 лет назад в записях Сринивасы Рамануджана. Здесь, по описанию компании, AxiomProver не просто закрыл пробел в почти готовом решении, а построил доказательство целиком, от начала до конца, а затем формально подтвердил его. Еще два доказательства, о которых говорится в статье, касаются вероятностной модели «тупиков» в теории чисел и инструментов, выросших из методов, которые в свое время помогали атаковать и в итоге решить Великую теорему Ферма.

Профессор Гарвардской школы бизнеса Скотт Коминерс, знакомый и с гипотезой Фела, и с технологией Axiom, называет результат впечатляющим не только из-за автоматизации и мгновенной проверки, но и из-за «элегантности и красоты» получившейся математики. Сам Оно считает, что такие системы обозначают новую парадигму доказательства теорем и могут подсветить более фундаментальный вопрос: можно ли сделать предсказуемыми те самые «ага-моменты», которые обычно считают чистой интуицией.

Чэнь, который увидел, как его собственная гипотеза превращается в доказанную теорему с помощью ИИ, смотрит на будущее скорее оптимистично. Он сравнивает ситуацию с появлением калькуляторов: математики не забыли таблицу умножения, но получили инструмент, который расширил возможности. По его мнению, ИИ может стать не просто помощником, а интеллектуальным партнером, который открывает более широкие горизонты для исследований.