Версия Markdown

AI-translated from English; not yet reviewed by a fluent editor.

# Математический репозиторий OpenAI: рукописи, версии и доказательства Lean

> В коллекции OpenAI — 722 рукописи из 372 семейств. На примере одной конфигурации доказательства Lean показано, как проверять версии, область действия и требования к проверке.

By BIG CHANGE Editorial

Published: 2026-10-07T04:13:00.689Z
Updated: 2026-10-07T04:13:00.689Z
Canonical: https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs

![Charcoal concept illustration of one reader holding loose manuscript folios, seen from behind, beside a second stack with an orange tab.](https://bigchange.ai/api/media/file/openai-math-manuscript-reading-hero-v1.png)
AI-generated conceptual illustration by BIG CHANGE.

Математическая публикация OpenAI от 6 октября открыла доступ к коллекции из 722 рукописей, объединённых в 372 семейства результатов. В одном семействе может быть несколько статей, а формальное доказательство может охватывать более узкое утверждение, чем связанная с ним рукопись. Проследив путь от статьи в репозитории до конфигурации её доказательства, можно увидеть, какое утверждение выбрали для проверки.

7 октября BIG CHANGE изучила полный список файлов репозитория, каталог и отдельные артефакты доказательств. Это документальный и статический анализ файлов; мы не собирали библиотеку Lean, не запускали проверку доказательств и не рецензировали математику. [Анонс OpenAI](https://openai.com/index/sharing-ai-progress-in-mathematics/) описывает развивающийся выпуск и обещает дальнейшие формализации.

## Главное изменение

- **Что изменилось:**Теперь исследователи могут проследить путь сотен созданных ИИ рукописей через общий публичный каталог к вспомогательным файлам, а для некоторых результатов — к формальным утверждениям и предлагаемым реализациям доказательств.
- **Почему это важно:**Математик, решающий, стоит ли использовать результат, может изучить утверждение, выбранное для проверки, его предположения и связь со статьёй. Структура репозитория помогает определить, где заканчивается более узкий формальный результат и начинается дальнейшая математическая экспертиза.
- **За чем следить:**OpenAI планирует добавлять формализации и сохранять редакции. Это важно всем, кто цитирует эту работу или опирается на неё: в обзоре нужно указать проверенные версию и теорему.

## Считайте рукописи и семейства отдельно

В нашем полном списке обнаружено 722 непосредственных каталога рукописей в `preprints/`; в каждом есть PDF. В `reasoning_traces/` найдено ещё 10 PDF. [Карта рукописей](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md) содержит 372 записи отдельных семейств и ссылки на 722 рукописи.

Эти числа описывают разные объекты:

| Артефакт | Что может изучить читатель |
| --- | --- |
| Семейство результатов | Группа связанных статей, включая дополнительные аргументы, следствия или альтернативные доказательства. |
| Рукопись | Отдельный математический документ со своими исходными файлами и данными цитирования. |
| Краткое изложение рассуждений | Сокращённое описание рассуждений модели по выбранному результату. |
| Артефакт Lean | Формальные определения, утверждения и предлагаемые доказательства, а также ссылки и конфигурации для проверки. |

Файл [README репозитория](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md) объясняет эти категории и предупреждает, что уровень верификации различается. Для некоторых результатов нет формализаций Lean, а OpenAI отмечает, что неформализованная работа может содержать ошибки. В самом [каталоге формализаций](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml) область указана как "Partial progress", а статус проверки — как `unchecked`. Это метаданные публикации, а не результат проверки, проведённой BIG CHANGE.

Публичные файлы доступны без аккаунта OpenAI. В анонсе говорится, что создавшая их модель является внутренней и что OpenAI работает над её выпуском. Поэтому доступ к документам не означает доступ к самой модели.

## Зафиксируйте версию, прежде чем изучать доказательство

Использованный здесь снимок репозитория соответствует коммиту [`adc7f1241b42e322a6451854ab7e4b4c146bf78a`](https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a) от 6 октября 2026 года, 21:58:50 UTC. Ссылки с этим идентификатором ведут к изученному снимку, а ссылки с `main` следуют за меняющейся веткой по умолчанию. README OpenAI обещает сохранять прежние выпуски при появлении исправлений или новых редакций.

Начните с [обзора](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf), где семейства сгруппированы по разделам математики, затем найдите нужную статью по карте рукописей. Сохраните имя её каталога, коммит репозитория и предоставленную в статье ссылку для цитирования. Дата рукописи может отличаться от даты публичного выпуска коллекции.

В семействе 003 есть статья с утверждением о свободной от нулей области правее 7/8, альтернативное доказательство для области правее 11/12 и отдельная статья о нулях Ландау — Зигеля. В [каталоге первой статьи](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md) указана дата 30 сентября и приведена ссылка BibTeX. Точная ссылка на статью помогает не смешивать эти утверждения.

На [странице области Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md) описано, какие утверждения охватывает формализация, что исключено и какие последующие приложения из статьи опущены. Там приведены отдельные утверждения для проверки результата о дзета-функции, L-функций Дирихле и Гекке, а также равномерного разрыва между действительными нулями. Проверка одного утверждения не подтверждает автоматически все пункты этой страницы.

## Проследите за выбранным утверждением до его конфигурации

В [инструкциях Comparator](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md) от OpenAI в качестве примера используется семейство 003. Comparator сравнивает предлагаемое доказательство Lean с заданным испытанием. В примере [конфигурация JSON](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json) выбирает одну теорему: отсутствие нулей у дзета-функции Римана, когда действительная часть её аргумента больше 7/8.

Конфигурация указывает на модуль испытания и отдельный модуль решения. Она допускает стандартные аксиомы `propext` , `Quot.sound` и `Classical.choice` , а параметру `enable_nanoda` задаёт значение `false` . Nanoda — независимая система проверки, которую может использовать Comparator; в предоставленной конфигурации она отключена.

В [файле испытания](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean) есть `sorry` — маркер Lean для незавершённого доказательства. Здесь у него конкретная роль: он задаёт утверждение для сопоставления. Документация Comparator допускает такой маркер в испытании, но требует корректного доказательства в решении. Наличие `sorry` только в испытании ничего не говорит об успешности отдельного решения. [Документация Comparator](https://github.com/leanprover/comparator#readme).

Для описанной локальной проверки нужны эта конфигурация, модули испытания и решения, а также их зависимости. В репозитории закреплён [Lean 4.34.1](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain). В [манифесте Lake](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json) зафиксированы ревизии зависимостей, в том числе Mathlib: `d13f23b723b8a846827a245b89c10fc7d3f11612`.

OpenAI требует добавить `comparator` , `landrun` и `lean4export` в путь поиска исполняемых файлов, а затем приводит команды для каталога `lean/` :

```sh
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json
```

Это инструкции издателя, а не команды, которые мы запускали. Версии трёх внешних инструментов там не зафиксированы. Актуальная документация Comparator требует совместимую версию `lean4export` и описывает требования песочницы, а также условия, при которых успешная проверка подтверждает соответствие испытанию, использование разрешённых аксиом и принятие ядром. В воспроизводимом отчёте нужно указать версии установленных инструментов и фактический вывод вместе с коммитом репозитория.

В [README библиотеки Lean](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md) рекомендуется собирать небольшие части большой библиотеки. Там же описаны ограничения Linux на отображение памяти, которые могут помешать полной сборке. Мы не измеряли локальное время выполнения или стоимость оборудования для этого примера.

## Оценивайте успешную проверку в заявленных пределах

В [справочнике по проверке Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/), версия 4.35.0-rc3 на момент просмотра, различаются принятие формального доказательства и интерпретация смысла теоремы. Эта версия документации не совпадает с закреплённой в репозитории цепочкой инструментов.

Успешная базовая проверка означает, что ядро приняло формальное утверждение с учётом определений, импортов и аксиом. В зависимостях всё ещё могут быть незавершённые доказательства. В Lean описана команда `#print axioms` для отображения использованных аксиом, включая `sorryAx` для незавершённого доказательства в цепочке зависимостей.

Более строгие проверки повторно запускают сохранённые доказательства или сравнивают решение с отдельно заданным утверждением. Они по-прежнему зависят от среды проверки и правильности выражения задуманного смысла. Поэтому в отчёте нужно указать точное испытание, разрешённые аксиомы и настройки внешнего проверяющего. Принятие ядром или совпадение с испытанием не доказывают принятие журнала и не означают, что формализовано каждое утверждение рукописи.

## Показатель вычислений описывает генерацию

OpenAI сообщает, что на средний результат затрачивались вычисления, эквивалентные примерно трём часам рассуждений ChatGPT Pro. В README сказано, что при оценке было задано около 4 000 задач, результаты затем сгруппировали и выбрали значимые. Также указаны исключения из обычной процедуры. Это данные компании о генерации; они не определяют стоимость проверки Lean читателем и не дают общей суммы в долларах. [Анонс выпуска](https://openai.com/index/sharing-ai-progress-in-mathematics/), [описание генерации](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced).

Для семейства 003 этот анализ выявляет конкретное утверждение о дзета-функции, предлагаемое решение и разрешённые проверяющим аксиомы. Он также подтверждает, что в примере Nanoda отключена. Успешность проверки с этой конфигурацией можно установить только запуском с записью результата.

## Источники и материалы для чтения

- [Анонс OpenAI от 6 октября](https://openai.com/index/sharing-ai-progress-in-mathematics/)Подтверждает дату выпуска, внутренний статус модели, запланированные дополнения и оценку вычислений компании. Это рассказ разработчика о собственной работе.
- [Закреплённый репозиторий](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a)Содержит каталог, файлы рукописей и конфигурации доказательств, изученные здесь. Подсчёты сделаны по полному списку файлов и карте рукописей; выбранные формальные файлы прочитаны без запуска. Для понимания структуры мы изучили исходник LaTeX обзора.
- [Справочник по проверке Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/)Объясняет смысл и ограничения проверки доказательств. Мы использовали версию 4.35.0-rc3; в проекте OpenAI закреплён Lean 4.34.1.
- [Документация Comparator](https://github.com/leanprover/comparator#readme)Описывает файлы испытания и решения, требования к среде и условные гарантии. Для этой коллекции результат проверки не приводится.
- [Обзор Кёртиса Пайка на Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/)Независимый статический анализ выпуска. В нём прямо сказано, что независимый запуск Lean не проводился; мы не считаем его воспроизведением проверки доказательства.
- [Предыдущая статья BIG CHANGE о математике и ИИ](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)Охватывает события с мая по сентябрь. В этой статье рассматриваются структура артефактов новой коллекции и процесс их анализа.

## Sources

- [Анонс OpenAI от 6 октября](https://openai.com/index/sharing-ai-progress-in-mathematics/) — Подтверждает дату выпуска, внутренний статус модели, запланированные дополнения и оценку вычислений компании. Это описание собственной работы разработчиком.
- [Закреплённый математический репозиторий OpenAI](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — Содержит каталог, файлы рукописей и конфигурации доказательств. Подсчёты основаны на полном списке файлов и карте рукописей; выбранные формальные файлы прочитаны без запуска. Для понимания структуры изучен исходник LaTeX обзора.
- [Справочник по проверке Lean](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — Объясняет смысл и ограничения проверки доказательств. Мы использовали версию 4.35.0-rc3; проект OpenAI закрепляет Lean 4.34.1.
- [Документация Comparator](https://github.com/leanprover/comparator#readme) — Описывает файлы испытания и решения, требования к среде и условные гарантии. Для этой коллекции результат проверки не приводится.
- [Обзор Кёртиса Пайка на Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — Независимый статический анализ выпуска. В нём прямо отмечено отсутствие независимого запуска Lean; мы не считаем обзор воспроизведением проверки доказательства.
- [Предыдущая статья BIG CHANGE о математике и ИИ](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — Охватывает период с мая по сентябрь. В этой статье рассматриваются структура артефактов новой коллекции и процесс анализа.