Джеймс Мэйнард и простые числа: задачи, которые ИИ пока не умеет решать

В 2013 году молодой британский математик Джеймс Мэйнард в одиночку совершил прорыв, над которым математики бились десятилетиями: доказал, что существует бесконечно много пар простых чисел, отличающихся не более чем на 600. Позже этот предел удалось снизить до 246. В 2022 году за это и другие достижения он получил медаль Филдса - математический аналог Нобелевской премии.

И вот вопрос, который сейчас реально обсуждается в математическом и AI-сообществах: мог бы ИИ сделать то же самое?

Если коротко - он придумал новое многомерное решето. Классическая задача теории чисел - "близнецы простых" (twin prime conjecture) - утверждает, что существует бесконечно много пар простых вида (p, p+2): например, 11 и 13, 17 и 19. Доказать это до сих пор не удалось никому. Но Мэйнард доказал нечто рядом: пар простых с разницей не более 600 - бесконечно много. Для этого он разработал новый инструмент - многомерное сито, которое значительно мощнее предыдущих методов.

Параллельно он решил гипотезу Даффина-Шеффера о рациональных приближениях и доказал результаты о больших пропусках между простыми числами. Всё это - задачи, где нет алгоритма перебора, нет готового пути. Только интуиция, новые конструкции и годы работы.

В 2024 году Google DeepMind представил AlphaProof - систему, которая решила несколько задач с Международной математической олимпиады (IMO). Это реально впечатляет: IMO-задачи требуют нетривиальных рассуждений, а не просто вычислений. AlphaProof работает в связке с формальным языком Lean, где каждый шаг доказательства верифицируется автоматически.

Но есть принципиальная разница между решением олимпиадной задачи и работой Мэйнарда:

- Олимпиадные задачи имеют красивое, компактное решение, которое можно найти за несколько часов. Математика на фронтире науки устроена иначе.

- Мэйнард не решал поставленную задачу - он придумал новый математический инструмент (многомерное решето), который открыл путь к решению. ИИ пока не умеет изобретать принципиально новые конструкции.

- Работа над гипотезой близнецов ведется десятилетиями. ИИ-системы пока не умеют работать в таком горизонте планирования.

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

Именно поэтому задачи класса Мэйнарда остаются вне досягаемости текущих систем. Не потому что у ИИ "нет интуиции" - это не точное объяснение. А потому что:

- нет обучающих данных нужного типа,

- нет механизма длительного исследования и накопления гипотез,

- нет способности изобрести новый формализм под конкретную задачу.

Несколько направлений развиваются активно. Системы формальной верификации (Lean, Coq, Isabelle) позволяют ИИ проверять и генерировать доказательства с машинной точностью. Проект Lean4 и связанные с ним LLM-инструменты уже помогают математикам формализовать сложные доказательства быстрее.

Терри Тао (другой лауреат медали Филдса) публично говорит, что ИИ уже полезен как "математический ассистент" - для проверки вычислений, поиска похожих лемм в литературе, быстрой формализации.

Но пройти путь от "ассистента" до "автора прорыва" типа работы Мэйнарда - это качественный скачок, который пока не случился.