OpenAI Publishes Ten Decade-Open Math Proofs, Each Formalized in Lean

OpenAI published ten new results in mathematics and theoretical computer science on August 1, 2026, each answering a problem that saw no progress on its main result for at least a decade. Every argument ships with a machine-checkable Lean 4 certificate, which is the strongest verification bar any AI-produced math has cleared at this scale.

What shipped#

The ten results span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography, and extremal combinatorics:

1. High-dimensional sphere packing: new upper bounds on density down to the Cohn-Elkies threshold.
2. Binary and spherical codes: exponentially improved bounds on maximum code size at any prescribed minimum distance.
3. Non-sofic groups: a construction proving such groups exist, resolving a central open question in group theory.
4. Connes's rigidity conjecture: a disproof, showing certain groups are not uniquely determined by their von Neumann algebras.
5. Arithmetic circuit complexity: new lower bounds for computing the permanent, including an n^4/log n formula lower bound.
6. Quantum parallel repetition: an exponential parallel repetition theorem for general two-player quantum games.
7. Closest vector problem: polynomial-factor hardness of approximation, a foundational lattice question with post-quantum cryptography relevance.
8. Ehrhart's volume conjecture: the maximum volume in every dimension for a convex body whose centroid is its only interior lattice point.
9. Multicolor Ramsey numbers: a superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.
10. Extremal number conjectures: results on the compactness and degeneracy conjectures, resolving Erdős problems 146 and 180.

The results were produced by an internal version of Astra, OpenAI's next major model, during development-time evaluation. OpenAI says the total tokens needed to find the solutions would cost roughly $2,000 at Sol API rates, putting the compute spend in a range any funded research lab could replicate. Humans then prepared the arguments into manuscripts using the same model, and the model formalized each one in Lean. OpenAI also released a reasoning walkthroughs PDF narrating the model's thinking process for each solution, plus the full paper.

Why the Lean certificates are the real story#

The GitHub repository is the part developers should inspect first. It is a standard Lean 4.32 project using mathlib and Lake: lake exe cache get && lake build All compiles all ten formalizations, and each result lives in a named module (NonSoficGroup.lean, ConnesRigidity.lean, Permanent.lean, GapCVP.lean, and so on). The repository is Apache-2.0 licensed, and a ComparatorChallenges directory provides independent proof-checking instructions.

That matters because machine-checked proofs change the verification conversation entirely. A human checking a 40-page proof takes months and can still miss a subtle gap. A Lean certificate compiles or it does not - the checker decides in minutes. This is the pattern we saw with the Cycle Double Cover proof in July, where OpenAI released both the proof and the prompt, and with the convex optimization gap closure that a researcher drove with a 10-page prompt. What is different here is scale: ten unrelated problems across eight fields, all formalized, not one flagship result.

My take#

Three things stand out. First, the breadth is more impressive than the depth. The unit-distance disproof in May was a single striking result; ten results across different areas in one release looks less like a lucky run and more like a capability. Second, the $2,000 compute figure matters because it prices the research method, not the result. At that spend level, theorem proving becomes a routine batch job any lab can run, and the constraint shifts to prompt design and result vetting rather than compute budget.

Third, the attribution stance is the part worth watching. OpenAI says it helped prepare the manuscripts and formalize the proofs, takes responsibility for their correctness, but states plainly that the mathematical arguments were generated by the system, and that claiming human authorship would misrepresent the system's contribution. That is a direct response to the Leiden declaration on AI and mathematics, which asks labs to disclose AI involvement. Expect this release to accelerate the norm where AI-generated results are labeled as such and verified formally rather than debated informally.

The formalization angle also strengthens the case for Lean as the lingua franca of AI math output. Mistral's open-weight Leanstral 1.5 already saturates miniF2F, and now the largest closed lab is publishing Lean certificates as its default artifact format. The tooling is converging even as the models diverge.

Continue Reading#

• GPT-5.6 Closes 30-Year Gap in Convex Optimization Theory - the earlier Lean-verified proof, driven by a domain-expert prompt
• GPT-5.6 Sol Ultra Produces Proof of the Cycle Double Cover Conjecture - OpenAI's first flagship AI math proof and the verification questions it raised
• Leanstral 1.5: Mistral's Open Theorem-Proving Model - the open-weight counterpart you can run locally
• Terence Tao Digests the Jacobian Conjecture Counterexample - how the math community reviewed a Claude Fable 5 result
• OpenAI's Efficiency Ledger - the cost and capability context behind Astra-class models

Sources#

• Ten advances in mathematics and theoretical computer science - OpenAI
• OpenAI ten-proofs repository - GitHub
• Ten proofs paper - OpenAI PDF
• Reasoning walkthroughs - OpenAI PDF
• Leiden declaration on AI and Mathematics
• ChatGPT for Academic Researchers - OpenAI