Ten proofs and the program that checks them

On 1 August 2026 OpenAI published Ten Advances in Mathematics and Theoretical Computer Science, 249 pages with ten results in mathematics and theoretical computer science obtained by one of its models, together with a repository holding a formal Lean 4 proof for each main result, one a machine can re-check. On the results themselves I have no standing to say anything. On the guarantee mechanism there is something to say, and the week the announcement lands in makes the question less theoretical than usual: on 28 July Lean shipped a patch for a soundness bug in its own kernel.

What the release contains

The abstract attributes the work to “an internal OpenAI model”; the announcement page names it, an internal version of Astra. The repository metadata records the framework as Codex and a wall time of one week. OpenAI states a compute cost of about $2,000 at Sol API rates for all ten results — a figure covering only the tokens needed to find the solutions, not training the model, and not the preparation of the manuscripts and the formalisation, which the company states as its own work.

The ten chapters, in the abstract’s own statements:

Sphere packing. The asymptotic strength of the Cohn–Elkies linear program determined exactly.
Binary and spherical codes. Classical upper bounds for fixed-distance binary and spherical codes improved by exponential factors for all parameters.
Non-sofic groups. An explicit non-sofic group constructed, settling whether every countable group admits finite permutation approximations.
Connes’s rigidity conjecture. Infinitely many pairwise nonisomorphic property-(T) groups constructed with the same group von Neumann algebra, and the conjecture falls.
Arithmetic circuit complexity. For the permanent, division-free circuits require Ω(n² log log n) gates and formulas Ω(n⁴ / log n) leaves.
Quantum parallel repetition. Exponential parallel repetition proved for every finite two-player entangled game.
Closest vector problem. A direct reduction from 3SAT gives n^(1/400)-factor hardness.
Ehrhart’s volume conjecture. The sharp bound (n+1)ⁿ/n! proved in every dimension, for convex bodies whose barycentre is their only interior lattice point.
Multicolor Ramsey numbers. A superexponential lower bound proves R_k(3) = k^Θ(k), which is Erdős problem 183.
Compactness and degeneracy. Two bipartite constructions disprove the compactness conjecture of Erdős and Simonovits and a degeneracy conjecture of Erdős.

What the kernel guarantees

A proof written in Lean is reduced to a proof term that the system’s kernel checks against the stated theorem. The kernel is small and independent of whoever wrote the proof: tactics, metaprograms and the elaborator all sit outside the trusted base, because whatever they produce still has to pass that check. If the kernel 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. This is the de Bruijn criterion, and it moves trust from whoever makes the claim to whoever checks it. It is what sets a release like this apart from a self-declared benchmark.

Four things the kernel does not cover.

The axioms. Mathlib adds three axioms to Lean’s type theory: propext, Classical.choice and Quot.sound. Only the second is classical in the proper sense; the other two concern extensionality and quotients, and are accepted in constructive mathematics too. If a file adds others through an axiom declaration, it is assuming something rather than proving it, and #print axioms on the theorem reveals it.

The shortcuts. A sorry left in a lemma lets through everything built on top of it, and does so almost silently: Lean emits the declaration uses 'sorry' warning only on the declaration containing the sorry, not on the ones that use it. Downstream it shows up in #print axioms, which reports sorryAx, and that is a value someone has to read, not an error that stops the build.

With a tactic such as native_decide the kernel checks none of the delegated computation: it accepts an axiom asserting the result, and the trusted base widens to the code generator, the runtime, and every definition marked @[implemented_by] or @[extern], which external checkers cannot revalidate. There has always been a trace in the axioms — up to 4.28.0 the single Lean.trustCompiler, and since 4.29.0 a dedicated axiom for each individual computation, checkable one by one.

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 leaves no trace anywhere and produces a theorem that is true and off target. The release contains a legible example: the non-sofic groups chapter says “an explicit non-sofic group is constructed”, while the Lean statement is an existence claim, ∃ (G : Type) (_ : Group G), Group.IsFinitelyPresented G ∧ ¬ Sofic G. Anyone checking it also has to read the definition of Sofic, which is written in the challenge file rather than taken from Mathlib.

What is left after the yes. Lean’s logical soundness is not provable inside Lean; the infrastructure running the check has to be uncompromised; no implementation defect may hit every checker at once. The manual lists these in full, and it is worth reading before saying that a certificate settles the matter.

The checker is software too

On 28 July 2026 Lean shipped 4.32.2, a fix-only point release. The notes read: “This point release fixes a soundness bug in the kernel. The issue was discovered by Ramana Kumar and reported by Kiran Gopinathan. A malicious meta program can trick the kernel into accepting a proof of False, or any other theorem. The kernel’s handling of nested inductive types with phantom type parameters was incomplete and bypassed the type checker.” The notes add that the bug could be exploited even when going through Comparator.

OpenAI’s repository pins leanprover/lean4:v4.32.0 in lean-toolchain, and the same revision for Comparator, both earlier than the patch. This is not a reason to doubt these ten proofs: the exploit requires a malicious metaprogram, and the ten main files contain no metaprogramming — no unsafe, no meta def, no @[implemented_by]. It is a measure of what kind of guarantee this is. The boundary is a program, and it holds until the right defect turns up in the right place — the same reasoning that applies to the sandboxes meant to contain an agent. The difference in the certificate’s favour is that here the defect was found, published with an issue number and fixed the same day, and anyone can re-run the check on an updated version.

What can be re-checked

The file formalization.yaml lists twelve main declarations with the exact name, the file containing each one and the axioms used. Twelve rather than ten because two chapters carry two each. Anyone wanting to check the translation has twelve statements to read rather than 249 pages.

Some things need stating precisely, because the release is more nuanced than the reporting around it.

The 249 pages never mention Lean. The pairing of each result with its certificate is asserted by the repository, not by the manuscript.
The certificates cover the main results, not every statement in the document. The arithmetic circuit chapter announces two bounds and only the one on formulas has a Lean declaration.
Comparator is the Lean FRO’s sandboxed judge: it compiles the solution in isolation, exports its environment and checks that the theorems prove the challenge file’s statement and use no axioms outside the permitted list. The independent kernel alongside Lean’s own is a separate program, nanoda, written in Rust, and all twelve configuration files enable it.
The closest vector problem challenge uses Comparator’s definition holes, for which the automated check only verifies that name, type and universe levels match. Comparator’s README warns that those solutions must always be checked by a further verifier, possibly a human one. The formal guarantee on that result is weaker than on the other eleven.
The ten main files contain no sorry, no axiom declarations and no native evaluation: this is verifiable with a grep over the clone, bearing in mind that the files under ComparatorChallenges/ do contain sorry by construction, since a challenge is precisely a statement without a proof.
In the same file the review field declares status: agent-reviewed, and there is no public record so far of anyone having run Comparator on these files. Peer review has yet to begin.

The May precedent

On 20 May 2026 an internal OpenAI model disproved a 1946 Erdős conjecture on unit distances in the plane, constructing sets of n points with n^(1+δ) unit-distance pairs for a fixed δ, with the explicit value of 0.014 pinned the same day by Will Sawin, in a paper already cited in the announcement. The problem itself stays open — the true exponent now sits between n^1.014 and the O(n^(4/3)) upper bound of Spencer, Szemerédi and Trotter — but the conjecture that the bound was n^(1+o(1)) has fallen. For eighty years the best lower bound was Erdős’s own √n × √n grid, with sub-polynomial growth in the exponent. Moving to a fixed δ is a different kind of step from a numerical improvement, and the method comes from number theory rather than combinatorics, which is probably why nobody in discrete geometry had found it.

That time verification was human and organised: OpenAI sent the proof privately to independent mathematicians, who published a companion paper of 19 pages signed by nine researchers, among them Noga Alon, Thomas Bloom, Tim Gowers, Daniel Litt, Jacob Tsimerman and Melanie Matchett Wood. Gowers wrote “a milestone in AI mathematics” there, Alon “an outstanding achievement”. The two phrases circulate on their own, and the paper containing them is more divided than that. It is Bloom who writes that some in the area will perhaps be a little disappointed with how little the result tells us, and that the original proof, while completely valid, “was significantly improved by the human researchers at OpenAI” and by the other mathematicians involved in the work.

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 has a property the first lacks: anyone can repeat it, as often as needed, without asking a mathematician for time again.

The Leiden Declaration

On 2 June 2026 a working group of sixteen people from fifteen institutions published the Leiden Declaration on Artificial Intelligence and Mathematics, which grew out of the Mechanization and Mathematical Research workshop held at the Lorentz Center in Leiden in September 2025 and was subsequently endorsed by the International Mathematical Union. Signatories include Terence Tao, Peter Scholze, Kevin Buzzard, and Scott Aaronson. It lists five threats:

Correctness. Plausible but unreliable arguments, hard to tell apart from correct proofs. This holds for formalisations too, where the difficulty lies in the translation between computer-encoded and human presentations of concepts.
Attribution. Models that do not cite the human work they synthesise, and data obtained by exploiting licensing arrangements made for other purposes, or by violating copyright.
Incentives. The use of AI rewarded for its own sake in hiring, funding, and recognition, to the disadvantage of those without access to it or unwilling to use technologies controlled by organisations whose values they do not share.
Evaluation. Results communicated through informal channels such as press releases and blog posts, on market timelines and before the mathematical community can apply its own processes.
Autonomy. Research questions chosen for their amenability to automation rather than by expert judgement of their significance.

The passage that describes the August announcement best, though, sits in the recommendations to industry. Mathematics is attractive to those building generalist models because “the correctness of formalized proofs can be checked automatically, without the need for human oversight”, which supplies a practically unlimited training signal on the assumption that capability developed on theorem proving carries over to general reasoning. The Lean certificate is at once the answer to the first threat on the list and the industrial reason these results exist. The warning against using specific mathematical tasks as a metric for the general reasoning capacity of a commercial product sits instead among the threats, in the fourth item, and lands squarely on the announcement.

The declaration is not a unanimous consensus. On 26 July Gowers explained that he took part in the workshop and did not sign, because in several places the declaration makes assertions and recommendations he feels uncertain about: he finds the very notion of proper evaluation problematic, since different mathematicians reach very different judgements without any of them being wrong, and parts of it strike him as oriented towards preserving the current state of affairs. He concludes all the same that the document is an important contribution. It belongs to the same genre as the framework Hassabis proposed in July, and should be read on the same criterion: what it states in observable terms, and what stays a principle.

The word singularity

On the Relentless podcast of 25 July 2026 Sam Altman said “this is the most interesting important thing I can imagine doing, and we are now like in the singularity”. This is not a new position for him: in the essay The Gentle Singularity of 10 June 2025 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 has a less tidy history than its use suggests. In 1965 I.J. Good described the intelligence explosion, a machine that designs machines better than itself, and that is a threshold one could in principle observe. Vernor Vinge’s singularity, codified in 1993, is defined the other way round, as the point beyond which the ability to predict the future breaks down, and by construction it is not verifiable. The two get used as though they were the same thing.

The figures cited in support do describe real growth, and they are worth taking at the source. The Anthropic Institute writes that as of May 2026 more than 80% of the code merged into Anthropic’s codebase was authored by Claude, noting in a footnote that the metric is the share of lines merged to production, and arguing in the same document that this is not yet recursive self-improvement, because goals, architecture and review remain human — a distinction that holds as long as verification has tools equal to the job. METR publishes the raw data for its 50%-success-rate time horizon: 3.95 minutes for Claude 3 Opus in March 2024, 60.4 minutes for Claude 3.7 Sonnet a year later, 718.8 minutes — just under twelve hours — for Claude Opus 4.6 in February 2026, with a confidence interval running from 5.3 to 60.6 hours and a warning that above sixteen hours the measurements are unreliable with the current task suite. The stated doubling time is 128.7 days counting models from 2023 onwards.

None of these numbers measures a system designing its own successor unaided. Altman himself puts the bottleneck in physical infrastructure: “There is relatively too much focus on algorithms that create better algorithms and not enough focus on data centers that can create more data centers”.

Market timelines

On 8 June 2026 OpenAI announced it had submitted a confidential S-1 to the SEC, writing “we expect it to leak so we’re just announcing it” and that the timing was undecided, “it may be a while because there are things we want to do that are likely easier as a private company”. The document is not public, because a confidential registration only appears on EDGAR once it is filed openly. On 9 July, asked whether the listing would come this year, Altman answered “I don’t know”; on 1 June he had called it “a financing event”. The same day, Anthropic had announced a confidential S-1 of its own. Both labs are on the way to a listing, and this is public knowledge.

That all of this bears on how research gets communicated is written into the Leiden Declaration, which names no company. The fourth threat describes publicity sought “on market timelines”, before the community’s processes of evaluation can take place. It recommends that policymakers not stop at press releases, because “there is currently a strong commercial incentive on the part of the technology industry to overstate the capabilities of their products”. The fifth threat carries the same effect into the university: with budgets under pressure, professional incentives push researchers to collaborate with technology companies “on asymmetric terms”, at which point the distortion reaches research and not only the market. Outside mathematics the pressure is measurable: on 9 July S&P downgraded Oracle to BBB-, one notch above speculative grade, citing the concentration of its remaining performance obligations on a single customer, which is OpenAI.

On this announcement I have nothing to offer. No source connects the 1 August release to a financing event, and on the declaration’s own criterion this case runs the other way, since it arrived with a manuscript and with certificates anyone can re-run rather than as a press release without disclosure. The structure does not change for one case that cuts against it, though, and we will have to get used to reading news of this kind, more and more often and with less and less time between the announcement and the moment someone actually evaluates it. The only thing I see working is the one this whole article is about, inside mathematics and outside it: asking first what comes attached that lets you check.

Cover image: P. Oxy. I 29, fragment of Euclid’s Elements with the diagram for Proposition II.5, first or second century AD — University of Pennsylvania, public domain — https://commons.wikimedia.org/wiki/File:P._Oxy._I_29.jpg