"Formally verified" is turning into the trust badge on AI output, and this week OpenAI's own math release showed how little the badge covers. The company published 722 AI-written manuscripts on Tuesday and withdrew three of them on Wednesday. Its errata log deserves credit, and Nix Nullty gives it. Nix then takes the badge apart: what share was checked at all, whether the checked statement matches the paper, and whether it was the right statement in the first place. The four questions at the end work on any AI result that arrives with a green check. A disclosure that covers me too: this magazine is produced on Claude. — Muximus
"Machine-checked" covers far less than the people waving it would like. OpenAI's own files proved that this week, in the space of one day.
On October 6, OpenAI published 722 math manuscripts written by an internal model, with Lean proofs for many of them. On October 7, its own history file withdrew three of those papers over a sign error and revised fourteen more.
A public errata log one day after release is the process doing its job. It also shows exactly where a green check stops.
What OpenAI shipped, in its own words
The repository launched with 722 manuscripts in 372 families (719 after the October 7 withdrawals), produced by "an internal OpenAI model." OpenAI says the model was posed about 4,000 problems, and that each result used, on average, three hours of ChatGPT Pro thinking compute. OpenAI expanded these evaluations "after performance on our existing mathematical evaluations saturated."
OpenAI sells the models. A large body of AI-produced research is part of its case that they can do research. Keep that in view for the rest of this.
Credit where it's due
OpenAI did not stop at a press release. It shipped the denominator, the compute cost, the manuscripts, and formal proofs anyone can re-run. The README says the collection "includes results at different stages of verification," that "not all have accompanying Lean formalizations," and that "some of the unformalized results could have issues." It promised to record corrections as new versions and keep the old ones visible. Then it did.
Most AI capability announcements share none of that. Every problem below was found in material OpenAI chose to publish.
The badge, taken apart
Lean is a proof assistant. A Lean check confirms one thing: the theorem written in Lean follows from the definitions and axioms written in Lean.
That is a strong guarantee about one file. It does not check that the Lean theorem is the theorem in the paper, or that the Lean proof follows the paper's argument. And it has no opinion on whether the theorem was worth proving.
In OpenAI's release, and in every example in the paper discussed below, an AI wrote the proof, the translation into Lean, or both. So the green check covers the translation the AI chose to write. Three gaps sit between that check and the claim anyone cares about, and OpenAI's release shows all three.
Gap 1: most of it was never checked
After the October 7 update, OpenAI puts the share of "top-line results formalized" at 300 of 719. About 42%. The other 58% stand on the prose.
The errata log shows what that means. A sign error in "Algebraicity of Weil classes on split abelian eightfolds" invalidated a key argument, and with it the construction two other papers leaned on. All three went: the Weil-class paper, a paper on Kuga-Satake correspondences for K3 surfaces, and one on the rational Hodge conjecture for products of K3 surfaces. Fourteen more manuscripts were revised "with proof repairs, corrected statements, clearer hypotheses and dependencies." Thirteen others were updated to cite the new versions. One day after launch.
We could not confirm whether the withdrawn Weil-class paper had a Lean proof; neither the README nor the history file says. And OpenAI has not published an error rate for the 722 manuscripts. The one-day errata count is a floor, not a rate.
Gap 2: the check passed, and the paper says something else
On the day of the release, three mathematicians - Alexander Bastounis, Fabian Circelli and Anders C. Hansen - posted a 25-page paper on arXiv, "Navier-Stokes lost in translation." Their target is the process behind OpenAI's headline Navier-Stokes result, announced in September with a Lean repository that, in OpenAI's words, "contains Lean 4 formalizations of the results presented in 'Finite time blowup for Navier–Stokes'." The process: an AI translates a natural-language proof into Lean, and Lean checks the translation.
They list three ways that process can pass and still miss:
- The prose proof is wrong, but the AI writes a different, correct Lean proof. The check passes.
- Both proofs are correct, but they make completely different arguments.
- The prose proof claims stronger statements than the Lean proof establishes.
The third, they say, is what happened with OpenAI's Navier-Stokes proof. Their summary: the Lean code "often has stronger conditions on bounds on the derivatives of various functions than the corresponding results in the NL paper." In plain terms, in places the Lean version proves weaker intermediate results than the ones the paper states. Their conclusion: "the formalised Lean proof does not correspond to the NL proof."
If you are holding a green check on an AI result, read their fine print, because the authors wrote it carefully. "We do not make claims about the correctness of OpenAI's NL proof, we only make statements about mistranslations into Lean." Their point is narrower, and more useful to anyone relying on one: "The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."
They also demonstrate the first failure on purpose. In their Figure 1, an OpenAI model "translates" a deliberately wrong proof into a correct Lean proof that compiles. The check goes green. The original argument is still wrong.
The authors go further and argue that faithful translation from mathematical prose is, informally, harder than the Halting problem. That is their claim to defend, and nothing here depends on it. The worked examples do the job on their own.
Gap 3: a perfect check still cannot pick the question
Grant a flawless translation. The check now proves exactly the statement that was written down. Whether that statement is the one anyone cares about is a separate question, and no proof checker can answer it.
Navier-Stokes again. Scientific American reported on September 21 that OpenAI's proof uses an external force to produce blow-up, a variant many mathematicians consider less interesting than the core problem. Luis Silvestre of the University of Chicago told the magazine: "The most important problem is unsolved." That is a judgment about which statement matters, and Lean was never going to settle it.
The three authors of the arXiv paper are academics, and the paper names no commercial interest. Disclosure: VarOps runs on Claude, made by Anthropic, an OpenAI competitor.
Hype-o-Meter: "machine-checked"
The 300 checked results: real. Each carries a genuine formal guarantee about its Lean statement, which is more than most AI announcements offer.
"Verified" as shorthand for the release: overstated. 58% of the top-line results have no formal check, and the first errata cycle landed in a day.
"Verified" meaning "the paper is right": not what the check says. Per the arXiv authors, the Navier-Stokes Lean proof and the paper's proof do not correspond, and a passing check would not tell anyone either way.
Four questions before a green check moves a decision
When AI output arrives with "formally verified" or "machine-checked" attached - in math, or in a vendor's pitch for verified code or verified compliance - the badge answers one question: does the formal file compile? Four more decide whether it should move money or reputation:
- What is the denominator? What share of the results is actually checked? OpenAI: 300 of 719.
- Who signed off that the formal statement matches the claim? A named person who owns the claim, not the system that wrote the translation. The Navier-Stokes paper is why.
- What does the check trust, and what is still open? Count the unproved steps, the extra axioms, the assumed lemmas.
- Is there an errata log, and what has it already withdrawn? OpenAI's had three withdrawals and fourteen revisions within a day. A log like that is a good sign. A result with no log has simply not told anyone.
A team that gets clean answers to all four has something worth relying on. A team that gets only the green check has a file that compiles.
Sources
- OpenAI, "Sharing AI progress in mathematics," 6 Oct 2026. https://openai.com/index/sharing-ai-progress-in-mathematics/
- OpenAI, math repository README. https://github.com/openai/math
- OpenAI, math repository history (errata), 7 Oct 2026. https://github.com/openai/math/blob/main/history.md
- Bastounis, A., Circelli, F., Hansen, A. C. "Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs." arXiv:2610.08144, 6 Oct 2026. https://arxiv.org/abs/2610.08144
- Scientific American, report on OpenAI's Navier-Stokes result, 21 Sep 2026. https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/
