News · 2026-08-03

Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs

Three days after OpenAI published ten mathematics and theoretical computer science results with machine-checkable Lean proofs, no one outside the company has publicly demonstrated that they compile. The repository has 434 stars and 39 forks, and exactly one commit. Pull requests are disabled, issues are disabled, and the Actions page shows no workflow runs. The audit trail the release invited has not appeared.

Key facts

• The openai/ten-proofs repository has one commit, 94bc0fe, dated 2 August 2026, with issues and pull requests both switched off.
• It carries 434 stars and 39 forks as of 3 August 2026. Forks record copying, not checking.
• OpenAI's announcement says the tokens needed to find the solutions would cost roughly $2,000 at Sol API rates.
• Primary source: the repository itself and its pull request and Actions pages.

The $2,000 number is the figure that traveled. It is real, it comes from OpenAI, and it means something narrower than the way it is being repeated. OpenAI's wording prices "the total number of tokens needed to find solutions to these problems" at the retail rate for its Sol model. That is a counterfactual API bill for the successful searches, not an audited compute ledger. At the published Sol price card, $2,000 buys on the order of 67 million output-priced tokens. What it does not include: every search that failed, the training that produced the model, the hardware, the energy, or the human mathematicians who, by OpenAI's own account, prepared the manuscripts before the model formalized them.

What is actually in the repository

The README lists the ten results plainly, and they are not small: improved asymptotic upper bounds on high-dimensional sphere packing, a construction of a non-sofic group, a counterexample to Connes's rigidity conjecture, an n^4/log n formula lower bound for the permanent, exponential parallel repetition for two-player quantum games, and counterexamples resolving two of Erdos's numbered problems, among others. Each maps to a Lean file.

The build path is documented and short. The project pins Lean 4.32.0 and mathlib, and you fetch the cache and run lake build All. OpenAI also ships a formalization manifest declaring that no result contains a sorry placeholder and that each depends only on Lean's three standard axioms. That is meaningful metadata. It is also OpenAI attesting to OpenAI's own work until somebody else runs the compiler.

How proof checking works, and what it proves

A proof assistant like Lean is a program that refuses to accept an argument unless every step follows from the rules. Think of it as a compiler for mathematics: if it builds, the reasoning is airtight, in the same way that a compiling program is syntactically valid. And in the same way, a compiling program can still do the wrong thing. The kernel checks that the proof establishes the statement written down. It cannot check that the statement written down is the theorem the mathematician meant.

That gap is exactly what the most substantive external engagement so far is careful about. A fork, jascal/ten-proofs-explained, builds Isabelle-checked structural skeletons of the arguments, and its README says outright that this is not a re-proof: the deep constructions and estimates are quoted as hypotheses, and no human expert has refereed the material. That is unusually honest, and it is engagement rather than confirmation.

Have any mathematicians weighed in?

OpenAI's manuscript thanks named specialists. Henry Bradford, Michael Chapman, Alon Dogon, and Francesco Fournier-Facio are credited with comments on the non-sofic groups chapter. Sorin Popa is credited with comments on the Connes rigidity chapter, and Francois Charles and Cyril Houdayer with careful readings. Those acknowledgments are documented pre-publication contact reported by OpenAI. None of them is a public statement by that person that a result is correct, and none covers all ten.

Why it matters

This is the cleanest available test of whether formal verification changes how machine-generated mathematics gets accepted. The whole promise is that a skeptic does not have to trust the lab, because the skeptic can run the compiler. Three days in, the compile-it-yourself artifact exists and the public receipt does not. That is not evidence the proofs are wrong. It is evidence that shipping a verifiable artifact and getting it verified are separate events, and the second one takes longer than a news cycle. Our earlier coverage of the announcement and of the non-sofic group result has the background.

The honest caveat: absence of a public build log is not proof that nobody has run the build. People compile things privately every day. What is verifiable is that the ordinary public signals of review, a CI badge, a build transcript, an issue thread, a named mathematician's assessment, are all still missing, and that OpenAI closed the two channels, issues and pull requests, where they would normally appear.

Primary source, verified: read the paper →

Ground Truth. (2026, August 3). Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs. Ground Truth. https://groundtruth.day/news/three-days-on-nobody-has-publicly-compiled-openais-ten-proofs.html

@misc{groundtruth:three-days-on-nobody-has-publicly-compiled-openais-ten-proofs,
  title  = {Three Days On, Nobody Has Publicly Compiled OpenAI's Ten Proofs},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {aug},
  url    = {https://groundtruth.day/news/three-days-on-nobody-has-publicly-compiled-openais-ten-proofs.html}
}

Topics: openai · mathematics · formal-verification · reproducibility · lean · evaluation