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.

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.