ten-proofs (OpenAI, 2026)

Apache-2.0 repo of Lean 4 formalizations for ten results in mathematics and theoretical computer science, released 2026-08-01 alongside OpenAI’s publication “Ten advances in mathematics and theoretical computer science” (openai.com/index/ten-advances-in-mathematics/, a paper and a set of reasoning walkthroughs). Lean 4.32.0 + mathlib, built with Lake; ten .lean modules plus All.lean; independent checking via the Comparator tool. ~380★ at ingest.

T1 — first-party on both halves (the repo and OpenAI’s own announcement, read directly). Also the rare case where tier barely matters: see lean-certificate.

What was claimed, in OpenAI’s words

“The results were achieved by an internal version of Astra, our next major model. The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates. These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate.”

So the division of labour is stated explicitly: the model generated the mathematics, humans and the model wrote it up, and the model also wrote the Lean. Each result additionally ships a narration of the model’s thinking.

The ten

High-dimensional sphere packing — new upper bounds on packing density down to the Cohn–Elkies threshold.
Binary and spherical codes — exponentially improved bounds on maximum binary-code size at any prescribed minimum distance, with spherical analogues.
Non-sofic groups — a construction establishing their existence, open since Gromov introduced soficity in 1999.
Connes’s rigidity conjecture — disproof.
Arithmetic circuit complexity — new lower bounds for the permanent, including an arithmetic-formula bound of order n⁴/log n.
Quantum parallel repetition — an exponential parallel-repetition theorem for general two-player quantum games.
Closest vector problem — polynomial-factor hardness of approximation (lattice-based post-quantum cryptography).
Ehrhart’s volume conjecture — the maximum volume, in every dimension, of a convex body whose centroid is its only interior lattice point.
Multicolor Ramsey numbers — a superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183.
Extremal number conjectures — compactness and degeneracy in extremal graph theory, resolving Erdős problems 146 and 180.

Not a benchmark suite: geometry, coding theory, group theory, operator algebras, complexity, cryptography and combinatorics, each a problem its own community had left open.

Why this lands hard in cluster E

alphaproof was the cluster’s evidence that deduction is being mechanized — an AI system solving competition problems whose answers were already known to exist. This is a different thing: open problems, chosen by their communities rather than by an examiner, with the argument produced by the model rather than a proof of a supplied statement.

And it arrives with the one property nothing else in this hub has. A lean-certificate moves the trust question out of the announcement and into a kernel: OpenAI’s word is not what you check, Lean’s is, and Comparator lets anyone do it on a laptop. Compare every self-reported number the hub holds — the router’s standing complaint that vendors measure on the sample that flatters them doesn’t apply, because the claim is not a percentage. It is a proof term or it is nothing.

What the certificate does not settle is whether the theorems are interesting, whether the proofs are illuminating, or whether the underlying arguments were reached the way the narrations describe. A kernel checks validity, not significance, and not provenance.

Against llms-cant-jump — a hard test, not a refutation

Six months earlier tom-zahavy argued that abduction — inventing the axioms — is structurally missing from these systems, with alphaproof cited as the deduction arrow being conquered. Ten open problems fell to a model in the interval. That looks like a refutation and is not one, for reasons Zahavy wrote into his own paper:

His scope is explicitly the physical sciences, and he says mathematics grounds “sense experience” differently.
He concedes that an LLM could plausibly execute the deductive phase given the premises.

Every one of the ten sits inside an established axiomatic system. Constructing a non-sofic group or disproving Connes rigidity is a search for an object or an argument within mathematics as it stands, not the invention of a new frame to reason from — closer to Einstein’s 1913–1915 grind, which Zahavy explicitly grants to machines, than to the “happiest thought” that preceded it. The honest verdict: the deduction arrow now reaches much further than cluster E had evidence for, and abduction is untested by this source rather than disproved. Recorded as a tension, not a win, in synthesis.

The attribution stance

OpenAI addresses authorship directly, naming the Leiden declaration on AI and Mathematics and its signatories: “claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.” They take responsibility for correctness; the arguments are credited to the system. Whatever one makes of the results, that is a clearer line than the field usually draws, and it is the seam to ../ai-governance-wiki (attribution and accountability as policy).

Precedent and aftermath

OpenAI’s May 2026 AI-generated disproof of the Erdős unit-distance conjecture is the stated precedent. The announcement footnotes five follow-on arXiv papers by human mathematicians (Bloom–Sawin–Schildkraut–Zhelezov on the sum-product conjecture over the reals; Pohoata on split primes and Elekes–Rónyai; Saha–Xu–Ye; Goh–Hatami; Lee–Pohoata–Zhu), which is the cluster-F question in live form: how fast does the community metabolize a result it did not produce.

Open

Astra is unreleased, so the cost figure (~$2,000 of tokens) and the capability claim can’t be reproduced by anyone outside OpenAI — only the proofs can. The canonical model node is astra in ../llm-providers-wiki (created 2026-08-03), which unpacks the cost figure as a token-volume proxy priced at GPT-5.6 Sol rates rather than an Astra price.
No independent mathematician’s assessment yet of whether the results are significant as mathematics, only that they are valid.

lean-certificate · lean-theorem-prover · alphaproof · llms-cant-jump · abduction · tom-zahavy · lean-for-programmers · synthesis