OpenAI’s largest mathematics release tackles 4,000 problems with Lean-checked proofs

OpenAI has released a large collection of mathematical research produced by an internal frontier model, giving mathematicians access to hundreds of machine-generated results.

The collection appears in a public GitHub repository with 722 manuscripts organized into 372 research families. The work spans pure mathematics, theoretical computer science, and mathematical physics.

Several results tackle problems that require lengthy chains of mathematical reasoning. OpenAI has also published formalized versions of many proofs in Lean, allowing computers to check the underlying arguments.

Hundreds of results

The repository covers problems involving number theory, complexity theory, geometry, and mathematical physics. Some results also extend into areas where small advances can require substantial technical work.

We’re releasing a broad range of new mathematical results produced by an internal frontier model.

We’ve been consulting with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study, and we have drawn on their advice and…

— OpenAI (@OpenAI) October 6, 2026

One example concerns the irrationality exponent of pi. That quantity measures how closely rational numbers can approximate pi. The model produced a result addressing the mathematical behavior of that approximation.

Another research family examines NP-hardness. These problems sit within computational complexity theory and concern tasks that are considered difficult to solve efficiently. The model’s work adds mathematical results to that broader body of research.

Other manuscripts address questions involving Mahler conjectures, arithmetic progressions and free group factors. The collection also includes work on quantum Heisenberg ferromagnets and relativistic Vlasov-Maxwell equations.

OpenAI has grouped related manuscripts into research families to show how individual results connect. The repository also identifies 10 families with abbreviated summaries of the model’s reasoning.

Lean adds a check

Lean provides an important verification layer for the release. The programming language lets researchers translate mathematical statements and proofs into formal code.

A computer can then check whether each logical step follows from the stated assumptions. That does not automatically establish that every research claim in the collection is correct.

Many manuscripts still lack formal Lean versions. OpenAI says it will add more formalizations as researchers complete the verification work.

The repository also tracks paper revisions and provides citation guidance. That gives researchers a clearer record when authors correct or expand an earlier manuscript. OpenAI developed the release process with advice from the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study.

Model tested thousands of problems

OpenAI also disclosed details about the scale of its mathematical evaluation. The model attempted roughly 4,000 problems during the research process.

An accepted result consumed about three hours of equivalent ChatGPT Pro thinking compute on average. OpenAI has also published additional statistics covering the attempted problems and research outputs.

The company says the reasoning summaries offer researchers a closer look at how the model approached selected mathematical questions. Those summaries remain separate from the formal proofs in Lean.

OpenAI plans to support workshops, conferences and special programs focused on understanding major mathematical results generated by AI. It also expects feedback from mathematicians to influence future disclosures.

The release therefore offers more than a collection of papers. It provides a test of how machine-generated mathematics can enter the research process with reproducible records, computer-checkable proofs, and greater visibility into how results