On 1 August, OpenAI announced its next major model by publishing a 249-page manuscript containing solutions to ten long-open problems in mathematics and theoretical computer science [2].
Consider the position that puts a reader in. The results span group theory, high-dimensional geometry, coding theory, quantum complexity, lattice cryptography and extremal combinatorics [2]. There is no living person qualified to referee all ten. There are probably fewer than a hundred qualified to referee any three.
So OpenAI shipped something else alongside the paper: ten machine-checkable proof certificates, one per result, written in Lean 4 [1].
That decision is the part of this story that belongs to us. Not the mathematics — almost nobody reading this constructs non-sofic groups for a living. The decision. When an agent produces output that outruns any available reviewer, you have two options: trust it, or make it prove itself to a machine.
What is actually in the repository
I went and looked, because the coverage of this announcement has been loose with details and the artifact is public.
github.com/openai/ten-proofs contains exactly what it claims: ten .lean files, one per result — SpherePacking.lean, NonSoficGroup.lean, ConnesRigidity.lean, QuantumParallelRepetition.lean, GapCVP.lean, and five more — plus an All.lean aggregator, a formalization.yaml, and the standard Lake build files. It is licensed Apache-2.0 and pinned to Lean 4.32.0 with mathlib [1].
That is a build, not a paper. You can clone it and run it.
Two files in that list do more work than they appear to. lean-toolchain pins the exact compiler version, and lake-manifest.json pins the exact mathlib revision the proofs were checked against [1]. Without those, a certificate rots: mathlib moves constantly, and a proof that verified against one revision may fail to compile against another for reasons that have nothing to do with whether the mathematics is correct. Pinning the toolchain is what turns "we checked this once" into "anyone can check this, in the same way, later." It is dependency hygiene applied to truth claims, and it is the difference between a verifiable artifact and a screenshot of one.
The README also points to reasoning walkthroughs and gives instructions for checking the formalizations with a tool called Comparator [1]. Shipping the check alongside the claim is a small thing that says something large: the burden of verification was moved to the reader on purpose, and made cheap enough that they might actually accept it.
The mathematics is genuinely hard. The construction of a non-sofic group settles a question open since Gromov introduced the concept, and the sphere-packing result improves a density bound that had not moved since 1978 [2]. Fields Medalist Tim Gowers said he would have recommended one of the proofs for publication without hesitation [2].
But the number everyone is repeating is the one that needs a qualifier.
The $2,000 is not what you think
OpenAI put the compute cost of the ten solutions at roughly $2,000, and that figure has travelled further than any other detail. It covers the successful runs, not every attempt the model made [2]. It is the cost of producing the published output, not the cost of the search that found it.
That is a meaningful difference. A number that excludes failed attempts describes publication, not discovery, and the two can differ by orders of magnitude in exactly this kind of search-heavy work.
Two more qualifiers, in the same spirit. Nine mathematicians were involved, and OpenAI staff helped prepare the manuscripts; the company's claim is that the mathematical content came from Astra, not that humans were absent [2]. And Astra itself is unreleased — it has no pricing, no benchmarks, and no availability. This is an announcement made through a demonstration.
I will also name something I deliberately left out. A claim circulating widely is that the repository's sorry count is zero — sorry being Lean's placeholder for an unproven step, so a count of zero would mean every step of every proof is machine-verified. It is a good detail. It is not in the README, which I read directly, and I could not confirm it [1]. So I have left it out. What is verifiable is that ten Lean certificates exist, publicly, under an open licence, and anyone can check them.
That last sentence is the whole point, and it survives without the statistic.
Why a checker beats a reader
A Lean certificate is not a summary of an argument. It is the argument, expressed in a language whose type checker will reject it if a single step fails to follow from the one before [2].
The checker has no opinion about where the proof came from. It cannot be impressed by fluency, and it cannot be tired at 4pm. It does not know whether a human or a model wrote the file, and its verdict does not change if you tell it. Feed it a proof with a gap and it fails, every time, in the same place.
This is a different kind of trust than the one software teams normally extend to AI output. The usual arrangement is a review: a person reads the diff and decides whether it looks right. That works because the reviewer can hold the change in their head. It degrades as the output grows, and it collapses entirely at 249 pages across six specialisms.
What replaces it is not a better reviewer. It is an artifact that carries its own proof of correctness — one that can be checked mechanically, cheaply, and by someone who does not understand the domain.
The ladder you already own
Formal proof is the strongest form of this move, and almost nobody needs it. But it is the top rung of a ladder whose lower rungs are sitting unused in most agent stacks.
Types. The weakest and cheapest. A typed interface rejects a class of wrong output before it runs, and it costs nothing at review time. Agents that emit code into a typed codebase are already being checked, continuously, by something that does not get tired.
Schemas. When an agent produces structured data, a schema turns "looks right" into pass or fail. The value is not validation. The value is that a schema failure is a machine-legible rejection the agent can be handed back, which turns a human review into a retry loop.
That loop is worth being concrete about, because it is the cheapest win on this list. An agent emits a record; the schema rejects it with a specific path and a specific violated constraint; that error goes back into the agent's context; the agent corrects and re-emits. No human touched it. The same failure without a schema produces a plausible-looking record that passes silently into storage and surfaces three weeks later as a support ticket. The schema did not make the agent smarter. It made the agent's mistakes addressable, which is the only property that scales.
Tests. The rung most teams stop at. A test suite is a set of claims about behaviour that a machine re-checks on every change. Its weakness is coverage: tests prove the cases you thought of.
Property checks. Stronger, and badly underused. Instead of asserting what happens for specific inputs, assert an invariant that must hold across all of them, and let a generator hunt for counterexamples. This is the closest most engineering work gets to the Lean posture — a claim about everything, mechanically attacked.
Proofs. Total, expensive, and appropriate when a wrong answer is unrecoverable: cryptographic primitives, consensus protocols, the arithmetic underneath money.
The pattern across all five is identical: push the checking out of the reader's head and into something the artifact carries with it. Every rung you climb buys back review capacity, which is precisely the resource that agents consume fastest.
The obvious objection is that formal verification has been available for decades and the industry has mostly declined to use it, because writing the specification is harder than writing the code. That has been true and it remains true for the top rung. What changed is the economics of the middle rungs. When a model will generate the property tests, the schemas, and the type annotations at negligible cost, the argument that verification is too expensive starts to describe a world that no longer exists. The bottleneck was never the checking. It was the writing of the things that get checked, and that is the part that just got cheap.
What a certificate cannot tell you
Lean will confirm that the sphere-packing bound follows from its premises. It will not tell you whether improving that bound was worth two thousand dollars of anyone's compute, or whether the ten problems chosen were the ten problems that mattered.
Verification is a check on correctness. It is silent on judgement.
That gap is where the work goes now. If a machine can certify that an agent's output is right, the scarce human skill stops being review and starts being selection — deciding what to point the thing at, and recognising when a technically flawless answer is answering the wrong question. Nine mathematicians did not become unnecessary in this story. They chose the problems.
The teams that adapt fastest will be the ones that stop asking their engineers to read everything an agent produces, and start asking them what would have to be true for the output to be wrong — then make a machine check exactly that.
A proof certificate settles the theorem. It has nothing to say about whether you should have asked.
References
[1] OpenAI — openai/ten-proofs: Lean certificates accompanying ten proofs in mathematics and theoretical computer science — (2026-08-01). Documentation
[2] Jon Markman, Forbes — OpenAI's Astra Solved 10 Decades-Old Math Problems For Just $2,000 — (2026-08-03). Article