Исследователи предложили LLM-конвейер для поиска крупных математических гипотез с проверкой в Lean 4
Авторы работы отмечают, что крупные математические гипотезы до сих пор формулируются в основном на интуиции экспертов, а единого метода для систематической генерации и проверки гипотез с серьёзным математическим потенциалом не существует. Чтобы закрыть этот пробел, они предложили трёхэтапный конвейер поиска крупных гипотез.
Первый этап, поиск в предметной области на основе модулей явных локальных свидетельств (region search from explicit local evidence modules): система ищет области, где могут находиться содержательные закономерности. Второй этап, рефлексивная проверка (reflective validation): кандидаты оцениваются на фундаментальность, новизну и потенциальную значимость. Третий этап, формальная проверка в системе Lean 4 с библиотекой Mathlib: гипотеза переводится в формальный язык и проверяется автоматическим ассистентом доказательств.
Цель конвейера, находить задачи с высоким «математическим вкусом» (problem taste): такие, доказательство которых способно переупорядочить язык целой исследовательской области и дать долговременную пользу математике, а не разовый результат.
Авторы протестировали конвейер на двадцати кандидатах-гипотезах. Все двадцать успешно прошли синтаксический разбор и проверку типов в Lean. Ни один из двадцати не был напрямую закрыт тактикой "exact?" и ни один не был автоматически снят тактикой "aesop", то есть кандидаты не свелись к тривиальным, уже известным системе утверждениям. Явных дубликатов или почти-дубликатов среди двадцати кандидатов авторы не обнаружили.
В тексте работы не названы ни авторы, ни их институты, ни дата публикации, ни конкретный пример найденной гипотезы (упоминание гипотезы Римана в заголовке, риторическое сравнение уровня амбиций, а не пример результата). Нет и сравнения с прежними автоматизированными системами поиска гипотез или доказательств.
Ключевые факты
- Трёхэтапный конвейер: поиск по локальным свидетельствам, рефлексивная проверка на фундаментальность/новизну/значимость, формальная проверка в Lean 4 и Mathlib
- Цель, находить гипотезы с высоким «математическим вкусом» (problem taste), доказательство которых меняет язык целой области, а не разовые технические факты
- На 20 тестовых кандидатах: 20 из 20 прошли синтаксический разбор и проверку типов в Lean
- 20 из 20 кандидатов не закрылись напрямую тактикой "exact?" и не были автоматически сняты тактикой "aesop", то есть не свелись к тривиальным утверждениям
- Явных дубликатов или почти-дубликатов среди кандидатов не найдено; конкретных примеров найденных гипотез в тексте не приведено
Почему это важно
Формулирование содержательных математических гипотез, задача, которая почти целиком держится на интуиции немногих сильных экспертов: работа отмечает, что единого систематического метода генерации и проверки таких гипотез до сих пор не было. Предложенный конвейер, попытка формализовать этот процесс и подключить к нему языковые модели вместе с формальным ассистентом доказательств, чтобы поиск гипотез не зависел исключительно от везения и опыта конкретного человека.
Кому это важно
В первую очередь, исследователям в области автоматизированного доказательства теорем и формальной верификации (сообщество Lean/Mathlib), а также математикам, которые могли бы использовать такой инструмент как источник кандидатов для дальнейшей проверки. Интересно это и разработчикам ИИ-агентов для науки: конвейер, конкретный пример того, как LLM встраивают в связку с формальным верификатором, а не оставляют её единственным судьёй правильности.
Как это применить
Практически метод описан как последовательность трёх шагов: сузить область поиска через модули локальных свидетельств, отсеять кандидатов рефлексивной проверкой на фундаментальность/новизну/значимость и лишь затем прогнать оставшиеся через формальную проверку в Lean 4 с Mathlib. Именно последний шаг даёт объективный, а не субъективный критерий: гипотеза либо синтаксически и типово корректна в формальной системе, либо нет. В тексте не указано, где взять код или как воспроизвести конвейер на своих данных.
Можно ли доверять
Источник, статья на arXiv, доступен только реферат (abstract) без полного текста, поэтому проверить методологию и результаты в деталях нельзя. В тексте нет имён авторов и институтов, нет даты, нет ни одного конкретного примера найденной гипотезы и нет сравнения с прежними системами того же назначения, это ограничивает возможность независимо оценить заявленные результаты. Выборка из двадцати кандидатов также невелика для выводов об общей эффективности метода.
Риски и подводные камни
Прохождение синтаксического разбора и проверки типов в Lean подтверждает лишь формальную корректность формулировки гипотезы, а не то, что она содержательна, важна или доказуема, само определение «фундаментальности» и «значимости» в тексте не раскрыто и остаётся оценкой самого конвейера. То, что тактики "exact?" и "aesop" не закрыли гипотезы автоматически, показывает лишь отсутствие тривиального решения, а не гарантию математической ценности. Без конкретных примеров и рецензии независимых математиков риск в том, что часть кандидатов может оказаться формально корректными, но не представляющими реального интереса формулировками.