LLM доказывают теоремы, но не открывают математику: исследователи описали следующий шаг

Группа исследователей опубликовала в начале июля 2026 года на arXiv позиционную статью, в которой систематизировала достижения LLM-теоремдоказывателей и выявила их принципиальный предел: нынешние системы доказывают теоремы, но не способны открывать математику — и предложила стратегическую дорожную карту перехода к полноценным исследовательским агентам.

Что умеют AI4Math-системы сегодня

За несколько лет LLM-системы для формальной математики добились ощутимого прогресса. Работая с языками интерактивного доказательства теорем (ITP) — в первую очередь Lean 4, Isabelle и Coq — они научились генерировать формальные доказательства для чётко поставленных задач. Эти языки позволяют записывать доказательства так, чтобы компьютер мог механически проверить каждый шаг — что делает результат принципиально надёжнее традиционных рукописных доказательств.

Авторы систематизировали три ключевых направления развития области:

• Датасеты — накоплены корпуса формализованных задач от школьного до университетского уровня, которые позволяют обучать модели на примерах правильных доказательств
• Автоформализация — модели улучшились в переводе условий задач, записанных на естественном языке, в строгий формальный синтаксис ITP
• Синтез доказательств — системы всё увереннее находят пошаговые доказательства при наличии чёткой исходной постановки

Все эти достижения объединяет одно: они работают только на хорошо определённых, заранее сформулированных задачах. Модель знает, что именно надо доказать, — и ищет путь к этой цели.

Почему это ещё не наука

Настоящая математическая наука принципиально отличается от решения задачника. Она требует умения формулировать гипотезы, выявлять неожиданные связи между разными областями и атаковать открытые проблемы — часто многолетние, нечётко сформулированные и предполагающие несколько уровней абстракции. Именно здесь нынешние LLM-системы демонстрируют системные ограничения.

Авторы выделяют пять ключевых проблем:

• Данные: датасеты не содержат примеров того, как рождаются новые теоремы — только решение уже поставленных задач
• Структура: математика опирается на сложные иерархии понятий и неявные зависимости между ветвями, которые LLM плохо усваивают
• Исследование: модели умеют отвечать на вопросы, но не формулировать новые — а именно это лежит в основе науки
• Инструменты: нет интеграции с системами компьютерной алгебры и специализированными математическими базами данных
• Коллаборация: модели не способны быть полноценным соавтором — они не понимают неформального контекста, который учёные передают друг другу

«Следующий прорыв в AI4Math требует решительного сдвига от решателей

предопределённых задач к исследовательским агентам, способным работать на переднем крае математики» — ключевой тезис статьи.

Какой должна быть следующая система

Стратегическая дорожная карта, описанная в статье, предполагает переход к математическим исследовательским агентам — системам, способным самостоятельно формулировать гипотезы, планировать исследовательскую программу, взаимодействовать с учёными в режиме диалога и итеративно уточнять постановку задачи.

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

Что это значит

Статья сигнализирует о важном сдвиге в горизонте задач AI4Math: от систем для верификации доказательств — к системам, способным участвовать в открытии новой математики. Этот переход требует принципиально иной архитектуры, чем масштабирование существующих подходов. Если предложенная дорожная карта будет реализована, математика может стать одной из первых областей, где ИИ выступит настоящим исследовательским партнёром учёного.