Пять лет назад математики Давэй Чен и Квентин Жандрон работали над сложной проблемой алгебраической геометрии, связанной с дифференциалами, то есть инструментами анализа, которые помогают измерять «расстояния» на искривленных поверхностях. В какой-то момент они сталкиваются с неожиданной проблемой: ключевой шаг основан на необычной формуле теории чисел, но исследователи не могут ни доказать, ни обосновать ее. Ведь результат должен был быть сформулирован как гипотеза, а не теорема.
Недавно Чен попытался вернуться к проблеме с помощью ChatGPT, часами обрабатывая запросы в надежде получить работающее доказательство, но заметного прогресса не добился. Поворотный момент наступил на математической конференции в Вашингтоне: там Чен встретил Кена Оно, известного математика, который недавно покинул Университет Вирджинии, чтобы присоединиться к стартапу Axiom. Компания разрабатывает инструменты искусственного интеллекта для доказательства теорем. Ее соучредителем является Карина Хонг, бывшая ученица Оно.
Чен рассказал Оно о своей нерешённой проблеме, и уже на следующее утро он получил готовое доказательство, которое сгенерировала система AxiomProver. По словам Чена, после этого «все естественным образом встало на свои места». Вместе с командой Axiom он оформил материал в статью, которая теперь опубликована на arXiv.
Как описывает Axiom, их инструмент находит связь между проблемой Чена и Гендрона и численным явлением, которое было впервые изучено еще в 19 веке. Затем система выдает доказательство и, что крайне важно для математики, независимо проверяет его правильность. Он утверждает, что искусственный интеллект заметил то, что упустили люди.
В Axiom утверждают, что это не единичный случай: за последние недели система предоставила им несколько новых свидетельств проблем, которые годами оставались нерешенными специалистами в различных областях. Речь все же идет не о самых известных и «дорогих» математических проблемах, а о вопросах, которые действительно затормозили прогресс в определенных областях. На этом фоне все больше математиков начинают использовать инструменты искусственного интеллекта не только для поиска идей, но и для доведения рассуждений до строгих, проверяемых доказательств.
Особый интерес представляет возможное применение таких подходов за пределами чистой математики. В документе упоминается перспектива разработки программного обеспечения, более устойчивого к определенным классам кибератак: если ИИ сможет создавать и проверять строгие доказательства, аналогичные методы можно использовать для формальной проверки кода, где правильность и надежность доказываются с помощью доказуемых свойств, а не тестов.
Подход Axiom построен на сочетании больших языковых моделей и AxiomProver, собственной системы рассуждений, усовершенствованной для получения доказательств, которые можно формально проверить.
Для этой цели используется Lean, специализированный математический язык и экосистема проверки. В компании подчеркивают, что это отличает их инструмент от «обычных» моделей ИИ: он не только генерирует текст, но и должен быть проверен в формальном представлении, что снижает риск красивых, но неверных рассуждений. Google продемонстрировал аналогичную идею с AlphaProof в 2024 году, и Хонг утверждает, что в их системе используются новые технологии и заметные улучшения.
Помимо истории с Ченом и гипотезой Гендрона, «Аксиома» приводит и другие примеры. Один из них связан с гипотезой Фелы о синергиях (сизигиях), т. е. конструкциях в алгебре, в которых отношения между выражениями «устроены» определенным образом. Примечательно, что в эту тему включены формулы, открытые более 100 лет назад в трудах Шринивасы Рамануджана. Здесь, по описанию компании, AxiomProver не просто восполнил пробел в почти готовом решении, а построил доказательство целиком, от начала до конца, а затем формально проверил его. Два других доказательства, упомянутые в статье, касаются вероятностной модели «тупиков» в теории чисел и инструментов, выросших из методов, которые когда-то помогали атаковать и в конечном итоге решить Великую теорему Ферма.
Чен, который увидел, как его собственная гипотеза превратилась в доказанную теорему с помощью ИИ, более оптимистично смотрит в будущее. Он сравнивает ситуацию с появлением калькуляторов: математики не забыли таблицу умножения, но получили инструмент, расширивший их возможности. По его словам, ИИ может стать не просто помощником, а интеллектуальным партнером, открывающим более широкие горизонты для исследований.
