OpenAI, ten mathematical results formalised in Lean: the role of the internal model

On 1 August OpenAI published the manuscript “Ten Advances in Mathematics and Theoretical Computer Science”, crediting the results to one of its own internal models. Alongside it came the GitHub repository `openai/ten-proofs`, which makes the Lean 4 formalisations of all ten proofs available. Among the results are an improved exponent for sphere packing — the first since 1978 — the construction of a non-sofic group, and a counterexample to Connes' rigidity conjecture. The repository is a Lean 4.32.0 project built on mathlib and released under Apache-2.0: anyone can recompile the proofs with `lake exe cache get` and `lake build All`, and a ComparatorChallenges folder explains how to run the verification independently.

Press reports have tied these results to “Astra”, the name of the next family of models OpenAI announced on that same 1 August; the manuscript, however, speaks only of “an internal model”, which has not been released. Figures such as the roughly 2,000 dollars in tokens or the document's 249 pages come from third-party reporting, since the official announcement page is currently unreachable. The paper thanks human mathematicians for proofreading and flags concurrent independent work by Shuoxing Zhou, developed in part with the assistance of GPT-5.6 Sol.

According to SiliconANGLE the mathematical arguments come from the model, but it was human researchers who turned its output into publishable manuscripts: how much that polishing weighs has not been quantified. The use of Lean 4 shifts the debate: a certificate guarantees the logical validity of a proof, but does not automatically confirm that the formalised statement coincides with the historical open problem — a check that remains a human job. None of the ten results has been through formal peer review. The precedent weighs heavily: in October 2025 the announcement that GPT-5 had “solved” ten Erdős problems turned out to be baseless, and Thomas Bloom, who curates erdosproblems.com, called it a serious misrepresentation. On today's ten results the same Bloom instead speaks of “big news”. As theoretical physicist Tobias J. Osborne notes, the 2,000 dollars quoted are the cost of the winning tokens, not the total haul of all attempts — a figure OpenAI has said nothing about. All of this lands in the context of the “Leiden Declaration on Artificial Intelligence and Mathematics”, published in June 2026 and backed, according to the-decoder, by more than 3,000 mathematicians and by the International Mathematical Union, which calls for transparency, protection of authors' rights and human responsibility for results.

The real news is not that a machine did mathematics — that has been happening for months — but that this time every result arrives with a recompilable Lean certificate: to judge it you don't have to trust whoever is making the announcement. Still, as long as the ratio of failed attempts to successes stays a trade secret, assessing how efficient these models really are will remain an exercise in faith rather than statistics.