OpenAI has published ten AI-generated results in mathematics and theoretical computer science, along with a public repository of Lean 4 formalizations.
The August 1 post frames the results as progress on problems that had seen no movement on their main result for at least a decade. OpenAI says the collection spans mathematics and theoretical computer science, including geometry, cryptography, and complexity.
The accompanying paper lists result families such as high-dimensional sphere packing, binary and spherical codes, non-sofic groups, closest-vector problem hardness, Ehrhart’s volume conjecture, and multicolor Ramsey numbers. The public openai/ten-proofs repository contains Lean files for the results and build instructions for checking them.
That makes this different from a normal model-capability post. OpenAI is not only saying a model can reason. It is publishing artifacts that mathematicians and formal-methods researchers can inspect.
The checkability is the news
AI math claims can go wrong in two ways. A model can write plausible prose that hides a bad proof, or it can solve a formal target that does not match the informal mathematical claim people care about.
The Lean repository helps with the first problem. A proof assistant can mechanically check whether a formal statement follows from its definitions and imported libraries. It does not, by itself, settle whether every informal interpretation is correct, important, or new.
That is why the repository structure matters. It names individual formalizations, points to the paper, and includes instructions for building all ten formalizations or a specific one. The next public review step is for domain experts to examine both sides: the formal Lean statements and the natural-language claims in the paper.
This is part of a larger math push
OpenAI’s post connects the new collection to its May 2026 unit-distance result and to the recent ChatGPT for Academic Researchers program. In that earlier unit-distance case, OpenAI said external mathematicians checked the proof and published companion material.
The new ten-result package raises the bar because it spans multiple areas rather than one discrete-geometry problem. It also makes formal proof infrastructure part of the release surface.
