Ten mathematical results with a Lean certificate

Artificial Intelligence

EU AI Act consulting: system classification, policies, AI governance, training.

Discover →

Research and Development

Applied research on AI, imaging and robotics, with clinical and academic partners.

Discover →

Today, 1 August 2026, OpenAI published ten mathematical results obtained by one of its models, each accompanied by a formal proof a machine can re-check. The part we are interested in is that last one: on the results themselves we have no standing to say anything, on the way they are guaranteed there is something to say.

What OpenAI published

The document is called Ten Advances in Mathematics and Theoretical Computer Science, runs to 249 pages and collects ten results on problems that, OpenAI writes, had seen no progress on the main result for at least a decade, and in most cases much longer. The abstract attributes the work to “an internal OpenAI model” without naming it, while the metadata in the formalisation repository records model Astra (OpenAI), framework Codex and a wall time of one week. According to trade press reporting, OpenAI puts the compute cost at about $2,000 at Sol API rates for all ten, a figure that excludes training the model and the surrounding human work.

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

1. High-dimensional sphere packing: the asymptotic strength of the Cohn–Elkies linear program determined exactly
2. Binary and spherical codes: classical upper bounds improved by exponential factors for all parameters
3. Non-sofic groups: an explicit non-sofic group constructed, settling whether every countable group admits finite permutation approximations
4. Connes’s rigidity conjecture: infinitely many pairwise nonisomorphic property-(T) groups constructed with the same group von Neumann algebra, and the conjecture falls
5. Arithmetic circuit complexity: for the permanent, division-free circuits require Ω(n² log log n) gates and formulas Ω(n⁴ / log n) leaves
6. Quantum parallel repetition: exponential parallel repetition proved for every finite two-player entangled game
7. Closest vector problem: a direct reduction from 3SAT gives n^(1/400)-factor hardness
8. Ehrhart’s volume conjecture: the sharp bound (n+1)ⁿ/n! proved in every dimension
9. Multicolor Ramsey numbers: a superexponential lower bound proves R_k(3) = k^Θ(k), which is Erdős problem 183
10. Compactness and degeneracy: two conjectures in extremal graph theory fall, Erdős problems 146 and 180

What a Lean certificate guarantees

A proof written in Lean 4 is reduced to a proof term that the system’s kernel checks against the stated theorem. The kernel is small, stable and independent of whoever wrote the proof. If it accepts, the theorem follows from the library’s axioms, and it makes no difference whether a mathematician, a student or a language model produced the text. Trust moves from the producer to the checker, and that is what sets a release like this apart from a self-declared benchmark.

Three things, though, the kernel does not cover.

The axioms used. Mathlib rests on three classical axioms, propext, Classical.choice and Quot.sound. If a file adds others through an axiom declaration, it is assuming something rather than proving it, and #print axioms on the main theorem reveals it.

The shortcuts. A sorry left in a lemma lets through everything built on top of it, and tactics such as native_decide hand part of the verification to the compiler, widening the body of code being trusted.

Statement faithfulness. The kernel guarantees that the proof proves the statement written in Lean. Whether that statement is the conjecture named in the title is a translation, and a person reads the translation. It is the step where an error produces no noisy failure but a theorem that is true and off target.

On the first two points the release is in order: the ten main files carry no sorry, no axiom declarations and no native_decide, and the metadata declares only the three standard axioms. The occurrences of sorry present in the repository sit in the ComparatorChallenges directory, which collects the challenges set up to have the proofs re-checked by an independent kernel, Comparator. These are checks anyone can repeat, and the instructions for a full build are in the README.

On the third point the release helps more than is usual: formalization.yaml lists twelve main results with the exact name of the Lean declaration, the file containing it and the axioms used, so anyone wanting to check the translation has twelve statements to read rather than 249 pages. In the same file the review field declares status: agent-reviewed, which places precisely where we are: peer review has yet to begin.

The May precedent

This is not the first result of its kind. On 20 May 2026 an internal OpenAI model solved the planar unit distance problem, posed by Erdős in 1946, finding an infinite family of constructions with n^(1+δ) unit-distance pairs for a fixed δ, later pinned down at δ = 0.014 by Will Sawin.

That time verification was human and organised: OpenAI sent the proof privately to independent mathematicians, who produced a 19-page companion paper signed by nine researchers, among them Noga Alon, Thomas Bloom, Tim Gowers, Daniel Litt, Sawin, Jacob Tsimerman and Melanie Matchett Wood. Gowers called it “a milestone in AI mathematics”, Alon “an outstanding achievement”.

Between May and August the way of guaranteeing a result changed, from a group of experts reading it to a certificate that re-checks itself. The two routes do not exclude each other, and the second costs far less for every result after the first.

The Leiden Declaration

The context this announcement lands in is not neutral. In June 2026 an international group of mathematicians published the Leiden Declaration on Artificial Intelligence and Mathematics, which grew out of a September 2025 workshop at the Lorentz Center of Leiden University and is endorsed by the International Mathematical Union, with signatories including Terence Tao, Peter Scholze, Kevin Buzzard and Scott Aaronson. It lists five risks:

• unreliable results, because a proof can look convincing and contain an almost invisible error
• missing attribution, with models producing results without citing the human work they build on
• dependence and inequality with respect to closed proprietary systems and expensive compute
• distorted incentives, with results communicated through press releases and blog posts rather than peer-reviewed journals
• loss of research autonomy, if questions get chosen because they are amenable to automation rather than because they are judged deep

On the first and second, today’s announcement answers with the certificate and with the citations: the repository declares the two Sphere-Packing-Lean projects it builds on, with author_contacted: yes and an explicit acknowledgement, and the Connes chapter notes that during preparation the authors learned of independent, concurrent work by Shuoxing Zhou, also a counterexample to the conjecture, developed in part with the assistance of GPT-5.6 Sol. On the third and fourth the announcement sits where the declaration fears, because the model is closed and internal and the channel is a company page with a PDF.

Altman and the word singularity

In the same week, on the Relentless podcast over the weekend of 28 July 2026, Sam Altman said: “We are now, like, in the singularity.” This is not a new position for him: in the June 2025 essay The Gentle Singularity he wrote “We are past the event horizon; the takeoff has started”, with the caveat that “of course this isn’t the same thing as an AI system completely autonomously updating its own code, but nevertheless this is a larval version of recursive self-improvement”.

The word does carry a technical meaning that is sixty years old and comes with a verifiable threshold, namely a system that improves its own successor without human direction. What Altman describes is rather a perceptual state, wonder turning into habit.

The figures cited in support describe real growth. Release intervals between frontier models compressed to about 60 days in 2026, against 315 and 195 days previously for Anthropic and OpenAI. Anthropic stated in May 2026 that more than 80% of the code merged into its production codebase is written by Claude. METR’s task time-horizon measurements, as reported by Forbes, go from about four minutes in March 2024 to ninety minutes a year later and twelve hours in early 2026. None of these numbers measures a system improving its own successor on its own, though, and OpenAI’s head of research Jakub Pachocki, on the same account, does not expect that by the end of the year. Altman himself puts the bottleneck in physical infrastructure, meaning data centres, energy and permits, rather than in algorithms.

What we think

On the ten results we are not in a position to judge, and the mathematicians who work on these conjectures have not yet had time to work through the arguments at the depth they usually require. What strikes us as interesting is the guarantee mechanism, because it resembles a problem we meet on a far smaller scale: giving a reader a way to check what is being claimed.

A Lean certificate is an artefact that is inconvenient for whoever produces it, because if the proof does not hold the kernel says no to anyone who runs it. Publishing it alongside the result seems to us the most solid part of the announcement, and worth more than the cost figure. What remains is the step nobody automates, reading the formal statement and deciding whether it is the right question, and it is the same asymmetry as in compliance audits, where a badly translated requirement produces impeccable evidence of something nobody needed.

The principle carries outside mathematics in a form we already know: a claim that brings along the artefact for checking it is worth more than a stronger claim without one. It is the same reason an SBOM counts for more than a security statement, and the December 2027 deadline of the Cyber Resilience Act asks for the inventory that lets someone verify rather than the promise that the components are in order.

On the singularity we would only note that the two claims of this week have different standing, because one can be run and the other describes a state. It is no reproach to Altman, who is speaking in images on a podcast, and it is only the reason why, when something has to be decided about a system, the useful question stays the measurable one: what does the system do that nobody asked it to do, and what does it leave behind so that someone else can check.

Sources

• OpenAI: Ten advances in mathematics and theoretical computer science
• The manuscript, 249 pages (PDF)
• openai/ten-proofs: the Lean 4 certificates on GitHub
• Comparator, the independent checker for the Lean kernel
• Leiden Declaration on Artificial Intelligence and Mathematics
• Leiden University: the declaration warns that AI is challenging the core values of mathematics
• The Next Web: OpenAI says its next model, Astra, has solved ten open problems in mathematics
• Forbes: Sam Altman Says We’re In The Singularity. What Does He Actually Mean?