В обновлении GitHub-репозитория с математическими формализациями OpenAI появились 6 новых Lean-формализацийзаписей доказательств на языке Lean, которые компьютер проверяет пошагово и без пропусков, 19 модификаций и 3 отзываУдаление ранее опубликованной рукописи из репозитория с математическими формализациями, подтверждённое в обновлении Dan Roberts. работ. Об этом сообщил Dan Roberts. После обновления репозиторий содержит примерно 42% формализованных top-line результатовКлючевые математические результаты, формализованные в репозитории, доля которых после обновления составляет примерно 42%.. Это первый случай, когда отзыв математических результатов OpenAI подтверждён конкретными числами и списком рукописей, а не общими формулировками.
Параллельно в открытых проектах описаны пайплайны, которые позволяют проверять выводы LLM формально — вплоть до принятия или отклонения доказательства ядром Leanпрограммой, которая механически проверяет каждый шаг доказательства и не пропускает логических пробелов. Ниже — что именно изменилось в репозитории, как устроена такая проверка и какие ограничения признают сами авторы инструментов.
Что именно изменилось в репозитории
Согласно обновлению Dan Roberts, в GitHub-репозиторий с математическими формализациями внесены 6 новых Lean-формализаций и 19 модификаций. Dan Roberts заявил, что репозиторий будет и дальше обновляться новыми формализациями и замеченными errata.
Отозваны три рукописи: Algebraicity of Weil classes on split abelian eightfolds, Algebraicity of Kuga–Satake Correspondences for K3 Surfaces и The rational Hodge conjecture for products of K3 surfaces.
Предыстория: что заявлялось раньше
1 августа компания опубликовала 10 результатов в математике и теоретической информатике. Вместе с анонсом OpenAI выложила 249-страничный отчёт со всеми доказательствами и формальными проверками. С августовскими десятью результатами OpenAI раскрыла намного больше: перечислила конкретные задачи, опубликовала работы и Lean-формализации.
В мае OpenAI сообщила, что её внутренняя модель опровергла гипотезу Эрдёша о единичных расстояниях — открытый почти 80 лет вопрос дискретной геометрии. 8 сентября OpenAI представила решение задачи существования и гладкости Навье—Стокса и опубликовала формализацию доказательства в Lean.
Позже OpenAI заявила, что внутренняя модель, обучение которой начали 28 августа, уже решила более 100 давних открытых задач почти по всем основным областям математики. Полный список задач, доказательства и методику подсчёта компания не публиковала. В этом сообщении нет такого уровня детализации, как в августовском. Часть результатов может потребовать доработки или независимой проверки.
11 сентября 25 математиков подписали декларацию A Severe Misalignment of AI in Mathematics, где указали на риски для атрибуции, научной коммуникации, образования и накопления математических знаний.
Как устроена проверка в LeanProofAgent
Пайплайн начинается с автоформализациипреобразования утверждения из естественного языка в формальное утверждение на Lean: из естественного языка генерируется одно утверждение теоремы на Lean. Затем Lean просят развернуть утверждение как пропозициюутверждение, которое может быть истинным или ложным и подлежит доказательству — это нужно, чтобы убедиться, что сгенерированное утверждение корректно оформлено как доказуемое. При ошибке elaborationразбора и проверки утверждения системой Lean управление возвращается к автоформализатору, а при валидной пропозиции переходят к генерации доказательства.
Доказательство генерируется LLM и проверяется ядром Lean через lake env lean. При неудаче модели возвращается точная диагностика компилятора для ограниченной попытки починки, и цикл повторяется. Опционально детерминированный лексический ретривер Mathlibбиблиотеки формализованной математики для Lean добавляет в промпт генерации доказательства реальные имена и сигнатуры локальных деклараций.
Принятое ядром доказательство становится финальным результатом. Ядро Lean — граница доверия к корректности доказательства, а не к семантической верности естественно-языкового утверждения. Все конфигурации, попытки, диагностики, задержки, использование токенов и итоговый результат сохраняются.
Какие ошибки отсекает Lean-проверка
Lean-проверка отсекает невалидный синтаксис, несуществующие библиотечные определения и некорректные утверждения. Языковые модели могут порождать правдоподобные математические аргументы, содержащие невалидный синтаксис, несуществующие API библиотек или тонкие пробелы в доказательстве.
Это происходит на нескольких этапах. Сначала утверждение, сгенерированное из естественного языка, проверяется Lean на этапе валидации утверждения. Если при элаборацииразборе утверждения Lean как пропозиции возникает ошибка, она возвращается автоформализатору. Затем сгенерированное доказательство проверяется ядром Lean, и при неудаче точная диагностика компилятора возвращается модели для ограниченной попытки исправления.
Среди конкретных наблюдаемых сбоев: текст в ограждениях или пояснения вместо утверждения или доказательства, несуществующие объявления и тактики Mathlib, реальные леммы с несовместимыми аргументами или типами, сбои тактик и нерешённые цели, формализации, отвергнутые при set_option autoImplicit false, лексический поиск, возвращающий нерелевантные посылки, стохастические регрессии и поиск доказательства эквивалентности, заканчивающийся unknown.
Мультимодельная проверка в PROOF-CHECKER
PROOF-CHECKER интегрирует несколько моделей — Gemini, GPT-4, Claude 3, Command R+, Mistral Large — и генерирует формальный код Lean4 из математических задач. Запросы к разным LLM выполняются параллельно для скорости, а ошибки обрабатываются через Promise.allSettledмеханизм JavaScript, который дожидается завершения всех параллельных запросов и собирает их результаты независимо от того, завершились они успешно или с ошибкой: он выбран потому, что при параллельном обращении к нескольким моделям часть запросов может завершиться неудачей, и такой механизм позволяет дождаться всех и учесть результаты остальных, не прерывая проверку из-за одного сбоя.
Human-in-the-loopподход, при котором человек участвует в проверке и оценке результатов системы реализован так: пользователю показывают несколько AI-решений, он выставляет оценку каждому по шкале 1–5 звёзд, а собранные предпочтения сохраняются для обучения моделей и создания датасетов RLHFобучение моделей на основе обратной связи от людей. Обратная связь отправляется через POST /api/feedback, где в теле передаются математическая задача, массив результатов и оценки по моделям.
Для конвертации задачи в Lean4 служит POST /api/verify: он принимает математическую задачу и возвращает список объектов с сгенерированным кодом Lean4, названием модели и признаком успеха, а также временную метку. Система обратной связи сохраняет ввод математической задачи, сгенерированный каждой моделью код Lean4, оценки пользователей от 1 до 5 звёзд, а также временную метку и метаданные. Для хранения доступны два варианта: Supabase (автоматическое сохранение в базу данных, доступ в реальном времени, удобные запросы и анализ) и EmailJS (уведомления по электронной почте, простая настройка, база данных не требуется).
Почему формальной верификации недостаточно
Формальная верификация в Lean выявляет конкретные дефекты: каждый кандидат проверяется в Lean, точная ошибка компилятора может быть возвращена модели для ограниченного исправления. Однако она не покрывает оценку математической ценности.
Быстрое получение доказательств уже поставленных задач не обязательно означает столь же быстрый рост человеческого понимания. Ценность для науки выше, когда системы находят новые методы, работающие за пределами исходных задач. Кроме того, сама проверка не является полной семантической валидацией: ограниченный поиск доказательств эквивалентности неполон и не является полной семантической валидацией. После автоматической проверки следует человеческий разбор, который может оказаться узким местом. Группа при IAS должна помогать оценивать значимость новых результатов и обсуждать их публикацию.
Что это меняет на практике
Для разработчиков, использующих выводы LLM в математике, обязательной практикой становится проверка каждого сгенерированного кандидата в Lean: каждый кандидат проверяется в Lean, точная ошибка компилятора может быть возвращена модели для ограниченного исправления, а все попытки сохраняются для инспекции.
Проверка включает генерацию одного Lean-утверждения из естественного языка, отклонение небезопасного выводаСгенерированный моделью текст, который отклоняется на этапе валидации утверждения перед тем, как Lean разбирает его как пропозицию. и просьбу к Lean разобрать утверждение как пропозицию, затем генерацию доказательства и его проверку через lake env lean. При неудаче возвращается точный диагностический вывод Lean для ограниченной попытки исправления, а также сохраняются конфигурация, попытки, диагностика, задержка, использование токенов и итоговый результат. Границей доверия к корректности доказательства объявлено ядро Lean, при этом корректность доказательства в Lean не равна семантической корректности на естественном языке.
Дополнительно предлагается опциональный инструмент — лексический поиск top-kотбор k наиболее подходящих по лексическому совпадению вариантов локальных деклараций Mathlib, чьи реальные имена и сигнатуры включаются в промпт доказательства. В PROOF-CHECKER предлагается система обратной связи человек-в-цикле: показ нескольких AI-решений, сбор предпочтений пользователей и сохранение отзывов для обучения моделей и RLHF.
Требования к воспроизводимости
Пайплайны проверки требуют, чтобы Lean 4 и Mathlib были зафиксированы на версии v4.34.0, а бенчмарк был заморожен и версионирован. Формальный бенчмарк содержит 18 замороженных задач, а его SHA-256 каталога равен 7ac68ea1e8fbad111763bf1b0b508253d91aa7a50bfccbc2879157ed7dc7f3d7.
Воспроизводимость обеспечивается записью в конфигурациях экспериментов точного Git-коммита, хеша бенчмарка, модели, лимитов попыток, переопределений генерации, тулчейнанабора инструментов сборки и компиляции, задающего версии компилятора и зависимостей проекта и таймаута. Сравнивать запуски разрешено только при совпадении промптов, лимитов попыток, Lean/Mathlib, хеша бенчмарка и конфигурации генерации модели. Сырые артефакты модели хранятся локально и игнорируются, а компактные отчёты и манифесты версионируются.
Цифры и метрики
Бенчмарк содержит 18 замороженных задач (лёгкие, средние и сложные случаи из арифметики, алгебры, логики, неравенств, множеств и функций). Прогоны используют не более трёх попыток формализации, трёх попыток доказательства и двух попыток эквивалентности на направление.
Сравнение моделей проводилось на локальных Ollama-настройках по умолчанию с одинаковыми промптами и лимитами, по одному прогону на модель:
| Метрика | qwen3:4b | qwen3:8b |
|---|---|---|
| Финальная успешность формализации | 16/18 (88.9%) | 17/18 (94.4%) |
| Успех доказательства с первой попытки | 3/18 (16.7%) | 3/18 (16.7%) |
| Финальная Lean-верифицированная успешность | 5/18 (27.8%) | 6/18 (33.3%) |
| Прирост от починки доказательств | +2 (+11.1 pp) | +3 (+16.7 pp) |
| Сквозная задержка | 7,083.47 с | 7,934.87 с |
8B-модель показала наблюдаемый прирост в одну верифицированную задачу при трёх выигрышах и двух регрессиях, что на 18 парах не является доказательством надёжного или статистически значимого улучшения, и заняла на 12.0% больше времени.
Эксперимент с поиском деклараций Mathlib проводился на qwen3:4b с фиксированным top-k 10: baseline дал 3/18 (16.7%) с первой попытки, 5/18 (27.8%) финально верифицированных, +2 (+11.1 pp) прироста, 13/42 (31.0%) галлюцинаций Lean/APIслучаев, когда модель ссылается на несуществующие объявления или тактики Lean и Mathlib на этапе доказательства и 7,083.47 с задержки; с поиском — 3/18 (16.7%), 7/18 (38.9%), +4 (+22.2 pp), 6/37 (16.2%) и 8,309.55 с, при этом зафиксировано 3 верифицированные регрессии.
Улучшение от поиска описано как наблюдаемое, а не статистически значимое: поиск выиграл пять случаев и потерял три, что дало чистый +2/18, при росте задержки на 17.3%. Поиск уменьшил число выдуманных имён API, но увеличил использование реальных, однако несовместимых лемм, и остаётся опциональным экспериментальным методом, а не значением по умолчанию в v1.0.
Важными метриками названы финальная Lean-верифицированная доля, успех с первой попытки, прирост от починки, сигналы отказа, число попыток, задержка и токены, сообщаемые провайдером, причём отсутствующие данные указываются как недоступные или как нижняя граница, но никогда не оцениваются.
Ограничения и открытые вопросы
Авторы признают, что формальный бенчмарк содержит всего 18 задач и по одному стохастическому запуску на основное условие, а выводы локальных моделей и задержка сильно варьируются от запуска к запуску. Ни одна модель не обучалась и не дообучалась в проекте, и ни одно улучшение не заявлено как статистически значимое.
Доминирующим узким местом названа генерация доказательства после того, как утверждение уже проходит Lean. Поиск доказательств эквивалентности неполон и не является полной семантической проверкой, а лексический поиск может возвращать нерелевантные посылки и вызывать регрессии.
Открытыми направлениями названы фильтрация посылок с учётом типов, поиск с учётом состояния доказательства, эмбеддинги теорем, более крупные воспроизводимые бенчмарки, обученные модели доказательства теорем и более сильная человеко-ориентированная семантическая оценка.
