# OpenAI's math repository: manuscripts, versions and Lean proofs

> OpenAI's collection contains 722 manuscripts in 372 families. A close look at one Lean proof configuration shows how to inspect versions, scope and checking requirements.

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's October 6 mathematics release gives readers a public collection of 722 manuscripts organized into 372 result families. A family can contain several papers, while a formal proof may cover a narrower statement than the accompanying manuscript. Following a paper through the repository to its proof configuration reveals which claim has been selected for checking.

BIG CHANGE inspected the repository's complete file inventory, catalogue and selected proof artifacts on October 7. This is documentation and static artifact analysis; we did not compile the Lean library, execute a proof checker or referee the mathematics. [OpenAI's announcement](https://openai.com/index/sharing-ai-progress-in-mathematics/) describes an evolving release and says further formalizations will follow.

## The big change

- **What changed:** Researchers can now trace hundreds of AI-produced manuscripts through a shared public catalogue to supporting files and, for some results, formal statements and proposed proof implementations.
- **Why it matters:** A mathematician deciding whether to use a result can inspect the statement actually selected for checking, its assumptions and its relationship to the paper. The repository's organization helps identify where a narrower formal result ends and further mathematical review begins.
- **What to watch:** OpenAI plans to add formalizations and preserve revisions. Those updates matter to anyone citing or building on this work: a review needs to identify the version and theorem it examined.

## Count manuscripts and families separately

Our inventory found 722 immediate manuscript directories under `preprints/`, each containing a PDF, and 10 PDFs under `reasoning_traces/`. The [manuscript map](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md) contains 372 distinct family entries and 722 manuscript links.

Those counts describe different objects:

| Artifact | What readers can inspect |
| --- | --- |
| Result family | A grouping of related papers, including companion arguments, consequences or alternative proofs. |
| Manuscript | An individual mathematical document, with its own source files and citation information. |
| Reasoning summary | An abridged account of the model's reasoning for a selected result. |
| Lean artifact | Formal definitions, statements and proposed proofs, with links and configurations identifying what to check. |

The [repository README](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md) explains these categories and warns that verification is uneven. Some results lack Lean formalizations, and OpenAI says unformalized work may contain issues. The [formalization catalogue](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml) itself records scope as "Partial progress." and review status as `unchecked`. Those fields are publication metadata, not the outcome of a checker run by BIG CHANGE.

The public files can be read without an OpenAI account. The announcement describes the generating model as internal and says OpenAI is working toward releasing it. Access to these documents therefore does not establish access to that model.

## Fix the version before following a proof

The repository snapshot used here is commit [`adc7f1241b42e322a6451854ab7e4b4c146bf78a`](https://github.com/openai/math/commit/adc7f1241b42e322a6451854ab7e4b4c146bf78a), dated October 6, 2026, at 21:58:50 UTC. Links containing that identifier preserve the snapshot examined here; links containing `main` follow the changing default branch. OpenAI's README promises to retain earlier releases when corrections or revisions appear.

Start with the [overview](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf), which groups families by mathematical subject, then use the manuscript map to reach a particular paper. Save its directory name, the repository commit and the paper's supplied citation. A manuscript date and the public collection's release date can differ.

Family 003 contains a paper claiming a zero-free region to the right of 7/8, an alternative proof for a region to the right of 11/12, and a separate paper on Landau-Siegel zeros. The [first paper's directory](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md) dates it September 30 and supplies a BibTeX citation. Recording the particular paper preserves the distinction between these claims.

Its [Lean scope page](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md) describes which statements the formalization addresses, identifies exclusions and says later applications in the paper are omitted. It links separate checking statements for the zeta result, Dirichlet and Hecke L-functions, and a uniform real-zero gap. A check of one selected statement cannot automatically stand for every item on that page.

## Follow the selected statement into its configuration

OpenAI's [Comparator instructions](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md) use family 003 as their example. Comparator is a tool for comparing a proposed Lean proof with a specified challenge. The example's [JSON configuration](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json) selects one theorem: the Riemann zeta function's nonvanishing when the real part of its argument exceeds 7/8.

The configuration points to a challenge module and a separate solution module. It permits the standard axioms `propext`, `Quot.sound` and `Classical.choice`, and sets `enable_nanoda` to `false`. Nanoda is an independent checker that Comparator can use; this supplied configuration does not enable it.

The [challenge file](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean) contains `sorry`, Lean's placeholder for an unfinished proof. That has a specific role here: it supplies the statement to be matched. Comparator's own documentation allows a placeholder in the challenge and requires a proper proof in the solution. Finding `sorry` in this challenge alone says nothing about whether the separate solution passes. [Comparator documentation](https://github.com/leanprover/comparator#readme).

For a documented local check, the inputs are that configuration, its challenge and solution modules, and their dependencies. The repository pins [Lean 4.34.1](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain). Its [Lake manifest](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json) records dependency revisions, including Mathlib at `d13f23b723b8a846827a245b89c10fc7d3f11612`.

OpenAI requires `comparator`, `landrun` and `lean4export` on the executable search path, then documents these commands from the `lean/` directory:

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

These are the publisher's instructions, not commands we executed. They do not pin versions of those three external tools. Comparator's current documentation requires a compatible `lean4export`, describes its sandbox prerequisites and specifies the conditions under which success establishes a match to the challenge, permitted axiom use and kernel acceptance. A reproducible report would need to record the installed tool versions and actual output as well as the repository commit.

The [Lean library README](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md) recommends compiling small portions of this large library. It also documents Linux memory-mapping limits that can prevent a complete build. We have no measured local runtime or hardware cost for this example.

## Read a successful check at its stated scope

Lean's [validation reference](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/), version 4.35.0-rc3 when consulted, distinguishes accepting a formal proof from interpreting the theorem's meaning. That documentation version is separate from this repository's pinned toolchain.

A successful basic check means the kernel accepted the formal statement under its definitions, imports and axioms. Dependencies can still contain unfinished proofs. Lean documents `#print axioms` to expose the axioms used, including `sorryAx` for an incomplete proof in the dependency chain.

Stronger checks replay stored proofs or compare a solution with a separately specified statement. They still depend on the checking environment and on the intended meaning being expressed correctly. This is why the exact challenge, allowed axioms and external-checker settings belong in a verification report. Neither kernel acceptance nor a match to a challenge establishes journal acceptance or that every claim in a manuscript has been formalized.

## The compute figure describes generation

OpenAI reports that the average result used computing effort equivalent to roughly three hours of ChatGPT Pro thinking. Its README says the evaluation posed approximately 4,000 problems, with outputs subsequently grouped and selected for significance. It also identifies exceptions to the usual procedure. These are the company's generation figures; they do not price a reader's Lean check or provide an aggregate dollar bill. [Release announcement](https://openai.com/index/sharing-ai-progress-in-mathematics/), [generation account](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced).

For family 003, this inspection identifies a particular zeta statement, the proposed solution and the checker's permitted axioms. It also establishes that the supplied example leaves Nanoda disabled. Whether that configured check succeeds remains a question for an executed, recorded run.

## Sources & further reading

- [OpenAI's October 6 announcement](https://openai.com/index/sharing-ai-progress-in-mathematics/) establishes the release date, the internal model's status, planned additions and the company's compute estimate. It is the developer's account of its own work.
- [The pinned repository](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) supplies the catalogue, manuscript files and proof configurations inspected here. Counts came from the complete inventory and manuscript map; selected formal files were read without executing them. We inspected the overview's LaTeX source for its organization.
- [Lean's validation reference](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) explains the meaning and limits of proof checking. We used reference version 4.35.0-rc3; the OpenAI project pins Lean 4.34.1.
- [Comparator's documentation](https://github.com/leanprover/comparator#readme) explains challenge and solution files, environment requirements and conditional guarantees. It does not report a verification result for this collection.
- [Curtis Pyke's Kingy.ai review](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) provides an independent static examination of the release. It explicitly reports no independent Lean execution; we do not treat it as reproduction of a proof check.
- [BIG CHANGE's earlier AI mathematics report](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) covers the May-to-September sequence. This article examines the new collection's artifact structure and inspection process.

## Sources

- [OpenAI's October 6 announcement](https://openai.com/index/sharing-ai-progress-in-mathematics/) — Establishes the release date, the internal model's status, planned additions and the company's compute estimate. It is the developer's account of its own work.
- [The pinned OpenAI math repository](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — Supplies the catalogue, manuscript files and proof configurations inspected here. Counts came from the complete inventory and manuscript map; selected formal files were read without executing them. We inspected the overview's LaTeX source for its organization.
- [Lean's validation reference](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — Explains the meaning and limits of proof checking. We used reference version 4.35.0-rc3; the OpenAI project pins Lean 4.34.1.
- [Comparator's documentation](https://github.com/leanprover/comparator#readme) — Explains challenge and solution files, environment requirements and conditional guarantees. It does not report a verification result for this collection.
- [Curtis Pyke's Kingy.ai review](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — Provides an independent static examination of the release. It explicitly reports no independent Lean execution; we do not treat it as reproduction of a proof check.
- [BIG CHANGE's earlier AI mathematics report](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — Covers the May-to-September sequence. This article examines the new collection's artifact structure and inspection process.