# OpenAI Mathematics Collection

> Source: https://aiwiki.ai/wiki/openai_mathematics_collection
> Updated: 2026-10-29
> Fact-checked: 2026-10-10
> Categories: AI Research, Mathematics, OpenAI
> License: CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) - attribute to "AI Wiki (aiwiki.ai)"
> Cite as: AI Wiki. "OpenAI Mathematics Collection." aiwiki.ai, 29 Oct 2026. https://aiwiki.ai/wiki/openai_mathematics_collection
> From AI Wiki (https://aiwiki.ai), the free encyclopedia of artificial intelligence. Reuse freely with attribution.

The **OpenAI Mathematics Collection** is a public collection of mathematical manuscripts and proof artifacts produced by an internal [OpenAI](https://aiwiki.ai/wiki/openai) model. OpenAI announced the release on October 6, 2026. Publication began a process of mathematical community assessment, rather than establishing acceptance of every result.[1][7]

## Scope and catalogue

The catalogue listed 719 manuscripts in 372 result families on October 10, 2026.[3] A family groups related work, which can include a principal result, supporting arguments, consequences, or alternative proofs.[2]

| Catalogue measure | Reported value |
|---|---|
| Manuscripts | 719 |
| Result families | 372 |
| Top-line results with formalizations | 300 of 719, approximately 42% |
| Revision history | Corrections and withdrawals recorded separately |

The catalogue sizes follow the overview; the formalization count and revision information come from the October 7 history notice.[3][4] The overview organizes families by mathematical subject rather than importance. Its disciplines include number theory, algebraic and complex geometry, analysis, theoretical computer science, combinatorics, mathematical logic, probability, mathematical physics, topology, and partial differential equations. Each family summary links to its associated manuscripts.[3]

## How the work was produced

OpenAI describes the collection as part of its evaluation of [mathematical reasoning](https://aiwiki.ai/wiki/mathematical_reasoning) on open research problems after existing evaluations saturated. The model attempted approximately 4,000 problems. OpenAI grouped selected outputs into families and manuscripts and applied a significance requirement, so the catalogue is a selected collection rather than a complete attempt log. Most results followed the same procedure using an unreleased internal model.[2]

The company estimates that the average result used computation equivalent to roughly three hours of ChatGPT Pro thinking. The release includes ten abridged reasoning summaries. These accompany selected results rather than every manuscript.[1]

## Reading and checking the artifacts

The repository provides an overview, a manuscript map, individual preprint directories, and a [Lean](https://aiwiki.ai/wiki/lean) library. Manuscript directories include citation and build instructions. OpenAI says revisions will retain earlier public versions and provides manuscript-specific BibTeX citations.[2]

| Repository resource | What it contains |
|---|---|
| `overview.pdf` and `overview.tex` | Subject-grouped descriptions of result families and links to manuscripts.[3] |
| `CONTENTS.md` | Individual manuscript titles, PDFs and abstracts, with links to available Lean coverage notes.[9] |
| `lean/formalization.yaml` | Machine-readable manuscript references, formal theorem declarations, Lean file paths and Comparator configuration paths.[10] |
| `lean/docs/` | Per-paper notes on the scope and limitations of formalizations.[6] |
| `history.md` | Dated withdrawals, repairs and additions to the formalization coverage.[4] |

The formalization catalogue labels its overall scope as partial progress. It records dependencies on existing libraries, including [Mathlib](https://aiwiki.ai/wiki/mathlib), rather than treating the supplied Lean files as self-contained proofs. Its entries identify particular declarations and comparison configurations, so a catalogue entry describes a specific formal artifact rather than a blanket status for every argument in a manuscript.[10]

The Lean library contains formalizations of some results and recommends compiling small portions rather than the entire library at once. Its documentation links to Comparator instructions for checking the supplied artifacts.[5]

Formalization coverage needs to be read at the level of the individual result. The Comparator documentation identifies several configurations that check supporting results rather than the corresponding paper's main theorem. Examples include seam compatibility in a character-variety construction and ring-theoretic properties of a completed surface cone. Those checks should not be described as formalizations of the full main theorem.[6]

### What a formal check establishes

Comparator checks a proposed Lean proof against a separately supplied challenge statement. Its configuration names the challenge module, solution module, selected theorems and permitted axioms. Under the tool's stated trust assumptions, successful checking establishes that the selected proofs match the challenge statements, use only permitted axioms and are accepted by the proof checker. The documentation also warns that challenges with open definitions can admit unintended answers and require additional review.[11]

Lean's documentation distinguishes checking a proof from deciding whether its formal statement expresses the intended mathematical claim. Definitions, notation, hypotheses and dependencies still need examination. An apparently completed theorem can depend on an unfinished proof or an added axiom elsewhere in its imports; axiom inspection is one of the checks the manual describes. Formal verification therefore supplies evidence about the precise statements and assumptions that were checked. It does not by itself settle the interpretation or mathematical significance of an entire paper.[12]

## Corrections and withdrawals

The history notice dated October 7, 2026 records three withdrawals. A sign error in the manuscript on algebraicity of Weil classes on split abelian eightfolds invalidated a cancellation argument and a construction used by two dependent papers involving K3 surfaces. The withdrawn directories retain explanations and links to the archived manuscripts.[4]

The same notice records substantive revisions to 14 other manuscripts, reference updates in 13 additional manuscripts, six new formalizations, and five additions covering supporting results.[4]

The repository warns that unformalized results may contain issues.[2]

## Mathematical community assessment

OpenAI consulted the independent [Advisory Group on Mathematics and Artificial Intelligence](https://aiwiki.ai/wiki/advisory_group_on_mathematics_and_artificial_intelligence) on release practices.[1] In its October 6 response, the group stated that its advisory role did not endorse OpenAI's process or judge the impact of the results. It described publication as the start of community assessment and human understanding, rather than completion of that work.[7]

The group's September 29 guidelines ask AI labs to stop testing advanced mathematics on proprietary models inaccessible to the community. They distinguish papers understood by a responsible mathematician from output that nobody yet understands. They call for precise statements, appropriate attribution, revision records, disclosure of the computational process, and clearly stated formalization coverage. They also recommend community-led support for developing human understanding and broad access to research tools.[8]

## Support for community understanding

On October 15, 2026, OpenAI updated the release announcement to state that it was contributing $5 million to a Simons Foundation initiative supporting the examination and development of AI-produced mathematics, including results in this collection.[1]

The Simons Foundation announced a broader partnership with [Anthropic](https://aiwiki.ai/wiki/anthropic) and OpenAI committing $15 million in combined funding and resources. The foundation would manage and award the funding, including through an open call for proposals. Planned support covered workshops and other initiatives for evaluating AI-assisted results, learning research tools and developing community standards. The two companies would also provide tools and computing resources to foundation-supported researchers, including researchers in basic science outside mathematics.[13]

## October 2026 additions

On October 26, 2026, OpenAI added two manuscripts with accompanying Lean formalizations to the repository. "Local smoothing for the Euclidean wave equation" claims to establish Sogge's [local smoothing conjecture](https://aiwiki.ai/wiki/local_smoothing_conjecture) for waves in every spatial dimension of at least two, which would also yield the [Kakeya](https://aiwiki.ai/wiki/kakeya_conjecture) maximal and dimension conjectures and Stein's spherical restriction estimates throughout the interior of the conjectured range. OpenAI released that output directly, as in the October 6 release.[4][14][15] "The Exponential Time Hypothesis is False" claims a deterministic algorithm that exactly counts satisfying assignments of fixed-width CNF formulas in subexponential time and polynomial space; its 3-SAT case would refute the [Exponential Time Hypothesis](https://aiwiki.ai/wiki/exponential_time_hypothesis).[4][16]

The additions came with a post, "Working with academic communities to build scientific understanding," in which OpenAI said it had asked outside experts to shepherd each new result. A group led by Russell Impagliazzo and Ramamohan Paturi (UC San Diego) and Ryan Williams (MIT) will verify and explain the ETH result and invited the community to help organize an open examination of the claim. At the group's request, OpenAI published the proof and Lean formalization immediately and committed to funding a conference on the result's implications.[14] The post also described a third result, a claimed existence proof for interacting four-dimensional quantum field theories including quantum chromodynamics. As a subproblem it includes a proof of the existence of pure Yang-Mills theory, part of the [Yang-Mills existence and mass gap](https://aiwiki.ai/wiki/yang_mills_existence_and_mass_gap) Millennium Prize problem. Its physics working group, led by David Gross, decided to hold off on releasing the AI-produced materials and to write the result up itself.[14] The same day, Anthropic released a separate paper, credited to Claude, claiming its own deterministic 3-SAT algorithm that refutes ETH.[17]

## References

1. OpenAI. [Sharing AI progress in mathematics](https://openai.com/index/sharing-ai-progress-in-mathematics/). October 6, 2026; updated October 15, 2026.
2. OpenAI. [Mathematics repository README](https://github.com/openai/math). Accessed October 10, 2026.
3. OpenAI. [OpenAI Research Catalog, overview source](https://github.com/openai/math/blob/main/overview.tex). Catalogue dated October 6, 2026; accessed October 10, 2026.
4. OpenAI. [Mathematics collection history](https://github.com/openai/math/blob/main/history.md). Revision notice dated October 7, 2026; additions entry dated October 26, 2026.
5. OpenAI. [Lean formalizations README](https://github.com/openai/math/blob/main/lean/README.md). Accessed October 10, 2026.
6. OpenAI. [Comparator challenges and supporting-result comparisons](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/README.md). Accessed October 10, 2026.
7. Advisory Group on Mathematics and Artificial Intelligence. [On OpenAI's release of mathematical results](https://agmai.org/). October 6, 2026.
8. Advisory Group on Mathematics and Artificial Intelligence. [Responsible release of AI-generated mathematics](https://agmai.org/general-sep29/). September 29, 2026.
9. OpenAI. [Mathematics manuscript map](https://github.com/openai/math/blob/main/CONTENTS.md). Accessed October 16, 2026.
10. OpenAI. [Mathematics formalization catalogue](https://github.com/openai/math/blob/main/lean/formalization.yaml). Accessed October 16, 2026.
11. Lean FRO. [Comparator documentation](https://github.com/leanprover/comparator). Accessed October 16, 2026.
12. Lean. [Validating a Lean Proof](https://lean-lang.org/doc/reference/latest/ValidatingProofs/). The Lean Language Reference, version 4.35.0. Accessed October 16, 2026.
13. Simons Foundation. [Simons Foundation Launches $15M Effort To Help Mathematicians Navigate AI Era](https://www.simonsfoundation.org/news/simons-foundation-launches-15m-effort-to-help-mathematicians-navigate-ai-era/). October 15, 2026.
14. OpenAI. [Working with academic communities to build scientific understanding](https://openai.com/index/building-scientific-understanding-with-academic-communities/). October 26, 2026.
15. OpenAI. [Local smoothing for the Euclidean wave equation](https://github.com/openai/math/blob/main/preprints/Local-smoothing-for-the-Euclidean-wave-equation-October-25-2026/paper.pdf). Manuscript in the openai/math repository, added October 26, 2026.
16. OpenAI. [The Exponential Time Hypothesis is False](https://github.com/openai/math/blob/main/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf). Manuscript in the openai/math repository, added October 26, 2026.
17. Anthropic. [A 2^o(n) Time Algorithm for 3-SAT](https://github.com/anthropics/formal-math/tree/main/eth), anthropics/formal-math `eth` folder (paper by Claude and Lean 4 formalization). Accessed October 28, 2026.