On 1 August 2026 OpenAI announced its next model family, Astra, by publishing ten new results in mathematics and theoretical computer science. Each was a problem open for at least a decade, and each shipped with a machine-checkable Lean 4 certificate.
The natural question, and the one we kept coming back to, is this: if nobody had solved these problems before, how do we know Astra is not just hallucinating a convincing fiction? The answer is that a Lean proof settles one kind of doubt completely and is silent on three others. Understanding which is which is the whole story, and it matters far beyond mathematics.
We build verification systems for regulated environments, so this question is our daily work. Here is the honest reading of what the Astra proofs establish and what they do not.
What OpenAI's Astra actually did
Astra produced ten results and OpenAI published the Lean certificates for all of them in a public repository under an open license. The list is specific and checkable: a construction of a non-sofic group, a counterexample to Connes's rigidity conjecture, a proof of Ehrhart's volume conjecture, new lower bounds for the permanent, hardness of approximation for the closest vector problem, exponential quantum parallel repetition, improved sphere-packing bounds at the Cohn-Elkies threshold, and resolutions of several Erdős problems including 146, 180 and 183. The whole compute run reportedly cost around 2,000 dollars. The repository reports that the number of unproven steps left open across all ten proofs is zero.
The important part is not the ten. It is that anyone with a laptop and the Lean compiler can verify each certificate independently, without trusting OpenAI at all.
Why the Astra proofs landed differently from the 2025 Erdős claim
OpenAI has stood on this stage before and fallen off it. In October 2025 the company said one of its models had solved ten Erdős problems. It had not. The model had retrieved existing solutions from the literature and presented them as new, and the mathematician who checked the work called it a dramatic misrepresentation. The claim rested on trusting the model's account of itself, and that trust did not survive contact with an expert.
The difference in 2026 is not a smarter model. It is that the model's word is no longer what you are asked to believe. Lean 4 is a proof assistant with a small, trusted kernel. A proof in Lean is not an argument that reads well. It is a term the kernel checks step by step against the axioms, and the verdict is binary. It compiles or it does not. There is no confident-sounding paragraph that slips past, no gap papered over with "and therefore, clearly." If the logic does not hold, it does not compile.
This is what a deterministic check looks like. The model is the probabilistic generator. The Lean kernel is the rule that is satisfied or it is not. The move that rescued a credibility crisis was simple: stop asking people to trust the model, and hand them a fact they can recompute themselves.
Can an AI hallucinate a math proof that still passes Lean?
For one specific kind of hallucination, the answer is no, and that is why this announcement carries weight. The failure mode where an argument is fluent and subtly invalid in the middle is dead. The kernel does not care how fluent a proof is. Every inference is mechanically checked, so a proof that compiles is logically valid by construction. That is as close to certainty as this kind of work gets.
But a green checkmark is silent on three other things, and each is a way to be wrong while compiling perfectly.
What a Lean certificate does not prove
The statement might not mean what you think. Lean proves a theorem. But that theorem is a formal statement a human wrote down. If the formalization of "there exists a non-sofic group" is subtly too weak, or quietly assumes something in a hypothesis, then Lean has faithfully proved the wrong thing, flawlessly. This is not a logic error. It is a translation error between the problem in English and the statement in Lean, and no amount of kernel checking catches it. Someone who knows both the mathematics and the formal language has to read the statement and agree it is genuinely the open problem.
A false axiom proves anything. The kernel builds on whatever axioms it is given. Add one bad axiom, by carelessness or design, and the system will prove any statement at all. Lean lets you print the full list of axioms a proof depends on, so this is checkable, but only if someone actually checks it.
Compiling is not the same as novel. This is exactly how the 2025 attempt failed. A proof retrieved wholesale from the literature compiles just as cleanly as an original one. Lean tells you a statement is true. It never tells you the statement is new. Only a specialist who knows the field can say whether a result is a genuine advance or a rediscovery.
The trust did not disappear, it moved
This is the point that generalizes. Verification did not remove the need for human judgment. It relocated it, and shrank it.
Before Lean, a mathematician had to read the entire argument and decide whether every step held, a large and fallible surface. After Lean, that whole burden is absorbed by the kernel. What remains for the human is narrower and sharper: does this formal statement match the real problem, and are its axioms honest? That is a smaller question, but not a less important one. It is the floor under the floor. The machine check is real, and underneath it sits an irreducible human check about what the machine was even asked.
The strongest version of this is in the repository itself. OpenAI did not only publish certificates that compile on its own machines. It included tooling for outsiders to independently re-run the checks. That is a deterministic floor made public and re-runnable, the most honest form the argument can take: do not trust us that it passed, run it yourself.
What this means for anyone building with AI
Most people reading this are not proving theorems. But the shape of the problem is the same everywhere AI touches something that matters. A model produces an output that is fluent and confident and might be wrong. The question is always the same: what checks it, and can that check be trusted more than the model itself?
The lesson of the Astra proofs is not that AI can now do mathematics, though it increasingly can. It is that the systems that earn trust are the ones that can point to a deterministic floor and say: here is the rule this had to satisfy, here is the proof it did, and you can check the proof yourself. And then, quietly, underneath that, a human who can confirm the rule was the right one.
Build the floor. Then remember the floor has a floor, and it is made of people who understand what the machine was actually asked to prove.
The Astra Lean certificates are at github.com/openai/ten-proofs and Lean itself is at lean-lang.org, both worth an afternoon.
So here is the question we would put to you: where in your own systems does the machine get the final word, and where does a person still have to confirm what the machine was even asked? We have been surprised, more than once, by where that line actually falls.
Top comments (0)