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 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 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 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 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, 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, 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 dates it September 30 and supplies a BibTeX citation. Recording the particular paper preserves the distinction between these claims.
Its Lean scope page 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 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 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 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.
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. Its Lake manifest 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:
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.jsonThese 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 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, 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, generation account.
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 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 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 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 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 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 covers the May-to-September sequence. This article examines the new collection's artifact structure and inspection process.
