Ten Proofs, Zero Sorries: What an AI Proof Certificate Actually Settles

In early August 2026, OpenAI published ten Lean 4 files on GitHub under an Apache 2.0 license. One of them formalizes the first explicit construction of a non-sofic group, a question that had stood open since 1999. You do not have to take OpenAI's word for any of it. You clone github.com/openai/ten-proofs, run lake exe cache get and lake build All, and either the Lean kernel accepts every proof or it points at the line where one fails. The model that produced these proofs, an unreleased system OpenAI calls Astra, is one you cannot run, cannot query, and cannot benchmark. The mathematics is fully checkable. The model is entirely opaque. That split is the whole story, and it is the cleanest illustration this field has produced of what an AI proof certificate does and does not settle.

This is the eval-honesty beat in its positive case, which this blog has spent a lot of words on from the negative side and never once from the positive. Usually the argument runs the other way: a leaderboard number is a hypothesis, not a result, because you cannot see the harness that produced it. Here is the exception. A machine-checked proof is a result, because the thing that certifies it is a small sound kernel you can run yourself. The interesting part is not that Astra is impressive. We have no way to establish that it is. The interesting part is that the impressiveness and the checkability come apart completely, and understanding why is worth more than any single one of the ten theorems.

The certificate, and what Astra shipped

Two things a result can ask you to trust

Every quantitative claim in machine learning asks you to trust something. The question that separates a result from a press release is what, exactly, and whether you can inspect it.

A leaderboard number asks you to trust a harness you cannot see. When a lab reports 77.6 on SWE-bench Verified or an Artificial Analysis index of 57, the number is the output of a pipeline: a prompt template, a scaffold, a sampling configuration, a grading script, a decontamination filter, and an assumption that the test set never leaked into training. Every one of those is a place the number can be inflated without anyone lying outright. The evaluation-crisis argument is that you are not being shown the pipeline, so the number is a claim about a system you cannot audit. You extend trust to the harness because you have no alternative.

A proof certificate asks you to trust nothing, or more precisely, to trust one thing that is small enough to check once and reuse forever: the proof checker. When Astra's output ships as a Lean 4 file, the claim is not "we ran an eval and it scored well." The claim is "this term has this type," and the Lean kernel is a few thousand lines of code whose entire job is to decide, mechanically, whether that is true. There is no prompt to leak, no grader to game, no distribution to overfit. Re-run the check on your laptop and you get the same verdict OpenAI got, because the verdict is a property of the file and the kernel, not of anyone's infrastructure. The trust you would have extended to a harness collapses to a one-time audit of a checker that the entire Lean community already audits continuously.

That is the inversion. It is not that certificates are a better kind of leaderboard. It is that they remove the leaderboard's load-bearing assumption (trust our measurement) and replace it with re-execution (run the measurement yourself). The diagram below is the whole idea.

What Astra actually shipped

Hold the framework for a moment and look at the instance, because the specifics matter and several of them are easy to overstate.

OpenAI's blog post, "Ten advances in mathematics and theoretical computer science," describes ten problems that an internal version of the unreleased Astra model closed, each formalized in Lean 4 and published in the openai/ten-proofs repository. The ten span high-dimensional geometry (the first improvement to the general upper bound on sphere-packing density since 1978), coding theory (binary and spherical codes), group theory (the non-sofic group construction), operator algebras (a disproof of Connes's rigidity conjecture), arithmetic circuit complexity (new lower bounds related to the permanent), quantum complexity (a parallel repetition theorem for two-player quantum games), lattice cryptography (a closest-vector-problem result relevant to post-quantum schemes), and extremal combinatorics (Ehrhart's volume conjecture, multicolor Ramsey numbers, and extremal-number conjectures, three of which sit in Paul Erdős's catalogue). The repository is Apache 2.0, pins Lean toolchain 4.32.0, and builds with lake build All. OpenAI's head of mathematics research, Sébastien Bubeck, confirmed the results publicly and noted that each ships with both a Lean certificate and a chain-of-thought walkthrough.

The headline is the non-sofic group. Soficity is an approximation property: a group is sofic if its multiplication can be approximated, in a precise finitary sense, by permutations of finite sets. The open question, traceable to work around 1999, was whether every group is sofic. No counterexample was known, and the absence of one had become its own small industry, because soficity implies several long-standing conjectures (Gottschalk's surjunctivity, Kaplansky's direct finiteness, forms of Connes's embedding program) for the groups that have it. Astra's result is the first explicit construction of a group that is not sofic. If it holds, it settles a question that had resisted 27 years of human effort, and it does so with a proof a machine can check line by line.

Two reported numbers are worth stating carefully because they are the ones most likely to get repeated without their hedges. The compute cost was reported at roughly $2,000, quoted at current GPT-5.6 Sol API token rates, which is OpenAI's figure and not something you can independently reconstruct from the repository. And the sorry count (Lean's placeholder for an admitted, unproven step) is reported as zero across all ten formalizations. Zero sorries is the load-bearing claim, and unlike the compute figure, it is one you can verify yourself. That is the entire point of shipping the files.

Where "trust the spec" finally has no gap

This blog argued, in the piece on verified code generation, that formal verification does not eliminate the trust problem, it relocates it. A verifier checks code against a specification and never checks the specification against your intent. Write a spec that says "sorted" as "non-decreasing" but forgets the permutation clause, and the checker will happily prove that a function returning the empty list is correct. The proof is sound. The spec is wrong. The unchecked link is the autoformalization step from human intent to formal statement, and that is where verified-wrong code enters.

Pure mathematics is the one setting where that gap closes, and Astra's certificates are the reason to make the point explicit. In application code, the specification is an intermediate artifact: a translation of what you wanted into what the verifier can read, and the translation can be wrong. In a mathematical theorem, the specification is the theorem. There is no intent sitting behind the statement ∃ G : Group, ¬ Sofic G that the statement might fail to capture, because that statement is itself the thing mathematicians care about. The formal object and the informal claim are the same object, written in two fonts. The relocation of trust still happens (you trust the statement, not the proof), but the destination is an artifact a competent reader can read in full in a few minutes, not a 2,000-line implementation and not a spec that might have paraphrased the goal incorrectly.

This is why the technique that certifies Astra's ten proofs does not port to your codebase, and saying so is not a hedge, it is the mechanism. The thing that makes a math certificate airtight (the spec and the claim being identical) is exactly the thing application code lacks. When you verify a payment kernel, the theorem is not "the code is correct," it is "the code satisfies this spec," and the gap between that spec and "the payments are actually right" is the whole risk. When you verify the existence of a non-sofic group, there is no daylight between the formal statement and the claim. Same tooling, same Lean 4, same sound kernel, categorically different assurance, because the unchecked link that haunts code verification is absent by construction here. If you take one transferable idea from the Astra release, it is this asymmetry, not the theorems.

The residual, and it is real, is that a reader still has to confirm the statement is the one claimed. A certificate for a weaker theorem type-checks just as cleanly as a certificate for the strong one. That is a human reading task, not a trust-the-lab task, and it is item three on the checklist below.

What the certificate does not settle

It says nothing about the model

Here is the discipline the coverage almost universally dropped, and it is the reason to write this piece at all. A certificate settles the claim and says nothing about the model.

Run the full list of what the ten proofs establish about Astra as a system, and it is empty. There is no hit rate: OpenAI did not report how many problems Astra was pointed at to produce ten it could close, so you cannot distinguish a model that solves these on the first attempt from one that fails on a hundred others that went unpublished. There is no attempt count per problem, which matters because test-time compute means the relevant quantity is often how many samples were drawn against a verifier, not whether the system "can" do it in some single-shot sense. There is no release date, no pricing beyond the retrospective token estimate, and a pending government security review: OpenAI has said it slowed Astra's deployment after internal evaluations flagged critical cyber capabilities, and is safety-testing with government agencies before broader access. So "Astra solved ten problems" is, as a statement about a capability, unfalsifiable. Nobody outside OpenAI can run the system, vary the problems, or measure the failure distribution. The one thing you can do is check ten specific proofs, and those ten proofs are mathematics, not a model.

This is not a complaint that OpenAI hid the ball. Publishing checkable certificates is more than almost any capability claim in this field ships with, and it deserves the credit. It is a precision point about what kind of object you are holding. The certificate is evidence about ten theorems. It is not evidence about a hit rate, a distribution, or a capability envelope, and the honest reading keeps those two ledgers separate. The mathematics moved from unverifiable to settled. The model stayed exactly as opaque as it was the day before, an internal system you are told about rather than one you can measure.

The failure mode to avoid is the natural inference "the proofs check out, therefore the model is as strong as advertised." The proofs checking out tells you these ten statements are true. It tells you Astra (or a human, or a search procedure, or some combination OpenAI has not itemized) produced ten Lean terms of the right types. It does not tell you the base rate, and in a field where the base rate is the entire eval-honesty argument, that omission is the number that matters. A model that closes ten famous problems out of a thousand attempts is a genuinely useful proof-search engine and also nothing like the impression "solved ten open problems" leaves. Both readings are consistent with the certificates, which is precisely why the certificates cannot adjudicate between them.

It says nothing about who proved it

There is a subtler version of the same confusion, and it is worth isolating because it is the one a careful reader falls into. Grant that the ten theorems are true. Who, or what, proved them?

The certificate is silent on this, and by design. A Lean file records that a term of the right type exists. It does not record how the term was found, how many dead ends preceded it, how much of the structure came from the model versus from mathlib's existing lemmas versus from a human curating and repairing the output. OpenAI's framing attributes the work to Astra, and Bubeck's walkthroughs describe the model's chain of thought, but the artifact you can check contains none of that. A proof produced by a model in one pass, a proof produced by a model inside a search loop with a Lean verifier pruning branches, and a proof produced by a model with heavy human steering all compile to the same certificate. The kernel cannot tell them apart, and neither can you from the file alone.

This matters because the interesting capability claim lives entirely in the provenance the certificate omits. "A system generated a checkable proof of a hard theorem" is a different and much stronger claim than "a checkable proof of a hard theorem exists," and only the weaker one is in evidence. When a result closes a problem that resisted human effort for 27 years, the natural question is whether the machine found the idea or formalized an idea it was given. The certificate answers neither. It answers the one question it was built to answer, which is whether the final object is valid, and that question is orthogonal to authorship.

Keep the provenance ledger separate from the validity ledger, then, the same way you keep the model ledger separate from the mathematics ledger. Validity is settled by the kernel. Provenance is settled by nothing you can run, which puts it in the same category as every other capability claim the field asks you to take on faith. The certificate does not launder an unverifiable capability claim into a verified one. It verifies a theorem and leaves the capability claim exactly where it found it.

How to read an AI proof claim

The next lab that announces a solved conjecture with a formal certificate will not necessarily ship one as clean as this. Treat any such claim as a certificate to audit, not a result to accept, and run the audit in this order. The first four items are mechanical and settle the mathematics. The fifth is the one that keeps you honest about the model.

1. Does it type-check under a clean build? Clone the repository, use the pinned toolchain (here, Lean 4.32.0 via lake exe cache get and lake build All), and confirm the build completes with no errors on hardware you control. A proof you cannot reproduce is a screenshot. If the build depends on a patched compiler or a non-standard fork of the checker, treat the whole thing as unverified until you understand the patch.
2. Is the sorry and axiom count actually zero? A single sorry admits an unproven step and voids the proof around it, so grep the sources and, more reliably, run Lean's own #print axioms on each headline theorem. The count you care about is not just sorry but the axiom set: a proof that silently leans on an extra axiom beyond mathlib's standard foundations is proving something in a stronger system than it appears to. Zero admitted steps and no non-standard axioms is the bar. Anything else is a footnote that belongs in the headline.
3. Are the theorem statements the ones claimed, and not weakened? This is the human-reading step the machine cannot do for you. Open the statement of each headline theorem and read it against the informal claim. Is the non-sofic group theorem stated for a group, with soficity defined the standard way, or has a definition been quietly relaxed so that a trivial object qualifies? A certificate for ∃ G, ¬ Sofic G is worthless if Sofic has been redefined. Check that the definitions are mathlib's or are themselves proven equivalent to the standard ones, and that no hypothesis has been added that trivializes the statement.
4. Are the definitions and imports the standard ones? A proof is only as meaningful as the library it builds on. Confirm the key definitions come from mathlib or a vetted source rather than a local file that could encode a convenient falsehood, and that nothing in the import graph overrides a standard definition. The soundness of the kernel does not protect you from a proof of the wrong statement.
5. Is compute and attempt-count disclosed? This item does not affect whether the mathematics is true, and that is the point of listing it separately. Once the first four pass, the theorems are settled regardless of what the model is. But if you want to say anything about the system that produced them, you need the hit rate, the attempts per problem, and the sampling budget. If those are absent (as they are for Astra), the correct statement is "these ten theorems are proven" and not "this model can solve open problems." Refuse to collapse the two. The certificate earns the first sentence and says nothing about the second.

The first four items are why the certificate is worth more than any leaderboard: they are checks you run, not trust you extend. The fifth is why the certificate is not a capability benchmark: the numbers that would make it one were never published. Both halves of that are the honest reading.

The general lesson worth keeping

Strip the specific theorems away and the durable idea is a way to grade claims by their auditability. A result you can re-execute beats a result you are shown, and the gap between them is not rhetorical, it is the difference between trusting a kernel you can read and trusting a pipeline you cannot. Proof certificates are the strongest version of re-executable evidence the field has, because the checker is sound and small and the claim is the theorem itself. That strength is real and it is narrow. It holds wherever the specification and the claim coincide, which is pure mathematics and a thin band of code where the property is the whole point (crypto primitives, memory safety, the cases the verified-code piece names). It does not extend to "the model is good," because "good" is a distribution and a certificate is a point.

The reason proof search became tractable at all is the same reason this discipline matters more now, not less: as models get better at producing checkable artifacts, the temptation to read the checkable artifact as proof of an unchecked capability grows in exact proportion. Astra's ten certificates are a gift to anyone who wants to know whether ten specific theorems are true. They are silent on everything else, and the silence is not a flaw in the release. It is the boundary of what a certificate can carry, and reading right up to that boundary and no further is the entire craft.

Key Takeaways

1. A leaderboard number asks you to trust a harness; a proof certificate asks you to trust nothing. The number routes through an unauditable pipeline of prompts, scaffold, and grading. The certificate routes through a small sound kernel you re-run yourself to reach the same verdict.
2. Astra's release is the positive case of eval honesty. OpenAI's unreleased model closed ten long-open problems (headlined by the first non-sofic group, open since 1999) and shipped a Lean 4 certificate for each, Apache 2.0, reported zero sorries, at a reported ~$2,000 of compute.
3. A certificate settles the claim and says nothing about the model. No hit rate, no attempt count, no release date, and a pending government security review, so "Astra solved ten problems" is unfalsifiable as a capability statement. The checkable part is the mathematics.
4. Pure math is the one place "trust the spec" has no gap, because the spec is the theorem. In application code the specification is an intermediate artifact that can misparaphrase intent. A mathematical statement is the intent, which is why certificates are airtight here and do not port to your codebase.
5. Zero sorries is verifiable; the compute figure is not. You can re-run the build and #print axioms yourself to confirm no admitted steps and no non-standard axioms. The ~$2,000 is OpenAI's own number and cannot be reconstructed from the repository.
6. The audit is four mechanical checks plus one honesty check. Type-checks under a clean pinned build, zero sorry and no extra axioms, the statements are the strong ones with standard definitions, imports are unmodified, and compute plus attempt-count are disclosed. The first four settle the math; the fifth is what stops you overclaiming the model.
7. Re-executable evidence beats shown evidence, and the strength is narrow. A certificate is the strongest re-executable claim available and it grades exactly one thing: the theorem. It is not a capability benchmark, because a capability is a distribution and a certificate is a point.