Skip to content
NewsResearch

OpenAI publishes Lean 4 proof certificates for 10 math results on GitHub, making claims machine-checkable

· by Pondero Newsdesk

The short version

Two days after its August 1 blog announcement, OpenAI released Lean 4 formal proof certificates to GitHub under Apache 2.0. The repository's sorry count is zero, meaning every proof step compiles without shortcuts.

OpenAI publishes Lean 4 proof certificates for 10 math results on GitHub, making claims machine-checkable

What separates OpenAI's August math announcement from prior AI-solves-hard-problem claims landed on August 3: a public GitHub repository, openai/ten-proofs, carrying Lean 4 formal proof certificates for all ten results, under an Apache 2.0 license. Each certificate compiles against the Lean kernel with a sorry count of zero, meaning no proof step was skipped or asserted without justification. Anyone with Lean 4 installed can now run lake build on the repository and independently verify every claim down to the kernel's logical axioms.

What the announcement covers

OpenAI's August 1 blog post, Ten advances in mathematics and theoretical computer science, described 10 results on problems that had stood open for at least a decade. Alongside the announcement, a 249-page manuscript and reasoning walkthroughs were released. Per OpenAI, the model inference used to find the solutions would have cost roughly $2,000 at Sol API rates; human researchers then helped turn the arguments into formal Lean code and prepared the manuscripts with the model.

Separately, The Information reported that the output came from "Astra," OpenAI's next major model still awaiting public release.

Headline among the ten results is an explicit construction of a non-sofic group, settling a question in group theory open since Mikhail Gromov introduced the concept of soficity in 1999. Also claimed: a disproof of Connes's rigidity conjecture on von Neumann algebras, an exponential parallel-repetition theorem for every finite two-player entangled game, and the first improvement to the sphere packing exponent since 1978, per Quartz, lifting it from about 0.5991 to 0.6044. Three problems from Paul Erdos's catalog were resolved as well, including the multicolor Ramsey problem (problem 183). Results span group theory, coding theory, quantum complexity, and high-dimensional geometry.

Why machine-checkable certificates matter

Verification of these results does not require trusting the model or OpenAI's narrative about how its model reasoned. Lean's kernel is a proof checker with a small, well-audited trusted codebase. A zero sorry count is binary: either every logical step across all ten proofs compiles, or it does not. Researchers who want to confirm the non-sofic group construction do not need to read the full 249-page manuscript; they download the repository, run the build, and observe the output.

Publishing under Apache 2.0 also lets other researchers extract sublemmas, extend results, or build on the formalized proofs without negotiating access.

One qualifier stands: OpenAI labeled the formalization status "agent-reviewed" in the repository manifest, not peer-reviewed. No chapter of the 249-page manuscript has been accepted at a journal or conference as of August 4. Outside specialists commented on individual chapters before release, including contributions on the non-sofic-group and Connes-rigidity chapters, but those contributions do not constitute formal acceptance. Confirming that each Lean statement faithfully captures what its corresponding open problem actually asked remains work for the mathematics community.

What to watch next

Community verification of whether the formal statements match the historically intended problems is already underway. A concurrent disproof of Connes's rigidity conjecture by researcher Shuoxing Zhou, reached with assistance from GPT-5.6 Sol, provides independent corroboration of the headline result, though it does not verify OpenAI's specific construction.

Formal journal submission and acceptance will determine whether any of the ten results enter the permanent mathematical record. OpenAI has not announced submission timelines. For practitioners watching AI capabilities, the Apache 2.0 release date and the zero sorry count are the durable facts; the peer-review status is the open question.

Sources