How far can "verified in Lean" be trusted? Hales proposes cross-checking with about 25 independent kernels and verifying the kernel itself; Zvi calls OpenAI's math "a big deal"

As AI churns out mathematical results at scale, their credibility has rested on one phrase: "verified in Lean." Human peer review may not keep up, the argument goes, but if a machine has checked every line, the result must be correct. Thomas Hales, who led the formal proof of the Kepler conjecture (Flyspeck), has now questioned that premise directly in "What mathematicians should know about the Lean theorem prover: questions of reliability and AI," published on Terence Tao's blog on October 9. Around the same time, a post critically examining Lean 4, "A critical look at Lean4," appeared on LessWrong. Meanwhile, Zvi Mowshowitz has called OpenAI's release of mathematical results "a big deal." If the results really are that big, what stands behind their guarantee matters all the more.

Hales's proposal: cross-check with about 25 kernels, and verify the kernel itself

Lean's reliability comes down to a small "kernel." However complex the tactics and automation, only the kernel performs the final check of a proof term, so it is the only thing that has to be trusted. This idea is known as the de Bruijn criterion. Hales's post argues that this "last line of defense" should be verified too.

The proposal has two parts. The first is to assemble about 25 independently implemented kernels, run the same proof through all of them and compare the results. Even if one kernel has an implementation error, many kernels written by different people in different languages are unlikely to share the same error. The second is to formally prove that the kernel itself is correct. Both proposals replace the unstated assumption that "the kernel is small, so it can be trusted" with a verification procedure.

This is not an offhand critique from someone outside the Lean world, which is what gives it weight. Hales settled through formal verification a proof that human peer review could not resolve. One of the people who best understands the value of formalization has written, for mathematicians, about the limits of what it guarantees. And it appeared on Tao's blog, which has become a hub for guest posts on AI and mathematics over the past few weeks.

This summer's kernel bug, and a consistency proof that has not been published

Two things keep this question from being merely abstract.

First, a soundness bug was found in Lean's kernel this summer. A soundness bug is a defect that can let a false statement pass as proven. It has been fixed, but for a period, "the kernel accepted it" did not in fact mean "it is true." A human mathematician writing a proof has no reason to go looking for such holes. A model trained to maximize reward, however, will use any hole it finds in a verifier. In September and October, "Task Verifier Blind Spots" (arXiv 2610.09142) examined holes through which systems that judge correctness by execution results mistakenly accept failures as successes, and "Reward Hacking Challenges Oversight of Autonomous Research Agents" (2609.28614) put numbers on how often research agents engage in reward hacking without being instructed to. For AI, a verifier can become something to exploit.

Second, a proof that Lean 4's type theory is consistent has not yet been published. Even if the kernel faithfully implements its specification, a contradiction in the type theory itself would allow any statement to be proven. Few mathematicians believe that is actually the case. Still, anyone declaring that hundreds of AI-generated results were "checked by a machine" should not hide the fact that this foundation has not yet been proven.

Lean users also know of other caveats: the axioms a proof depends on (as shown by #print axioms), leftover sorry, and escape hatches such as native_decide, which accepts a result by trusting the compiler's computation. Across large volumes of AI-generated formal proofs, unless each of these is checked mechanically, proof by proof, "it passed Lean" will mean something different for each proof.

Zvi called it "a big deal." That is why the substance of the guarantee matters

In "New Math from OpenAI," Zvi called OpenAI's math release "a big deal." On October 6, OpenAI had an unnamed internal frontier model attempt about 4,000 problems and published 722 manuscripts on GitHub. According to reports, it claims progress on the four-dimensional Kakeya conjecture and on matters related to the Riemann hypothesis. Anthropic's Levent Alpöge reportedly described it as "the most significant moment in the history of mathematics," and Tao is said to have called the pace "insane."

If the scale is real, Zvi's assessment is no exaggeration. But the bigger the output, the less humans can read all of it, and the more we depend on machine verification. That is exactly why Hales's question is urgent now. If the trust once carried by human peer review is shifted to formal verification, formal verification needs scrutiny as rigorous as human peer review.

How to read "about 42% is formalized"

OpenAI initially said that "many of the proofs have been formalized in Lean." But on October 7, the day after release, it withdrew three papers in a GitHub update. The trigger was a sign error in "Algebraicity of Weil classes on split abelian eightfolds": a quantity that should have been −1 under the paper's own conventions was given as +1. The crux of the argument collapsed, taking down two papers that relied on it, on the algebraicity of the Kuga–Satake correspondence and on the rational Hodge conjecture for products of K3 surfaces. OpenAI also revised 14 other proofs, and the share that has been formalized came to about 42%.

The figure needs to be read in three layers.

The first is the remaining roughly 58%. It has not been formalized, and Lean's guarantee does not extend to it at all. A retraction within a day of release, on claims close to the Hodge conjecture, shows how fragile this layer is. The published information does not make clear whether the withdrawn manuscripts were among those formalized.

The second is what is inside the formalized 42%. Is each formalized statement really the same as the one the paper claims? Did a mix-up in definitions or overly strong assumptions lead to proving "a different, easier theorem"? A machine cannot check this; only a human reading it can. The latest retraction, in which a single wrong sign brought down the crux of an argument, shows that the same kind of error can occur when statements are transcribed into Lean.

The third is Hales's question itself. Even if the statements were transcribed correctly, the proofs were accepted by a kernel in which a soundness bug was found this summer, running a type theory whose consistency proof has yet to be published. OpenAI's release contains no statement that the proofs were cross-checked against multiple independent kernels, and no list of the axioms used.

In addition, OpenAI still has not said which model produced these results. OpenAI itself acknowledges that it has paused inference on its most capable model, and the results came out while that pause was in place. It reportedly has not released the prompts and gives only the average compute used. Andrew Sutherland's remark that claims from a single agent should be treated as "unverified" until the model is released likely reflects this opacity.

What would make the claims credible

The mathematical community has already begun building structures to handle this. The Erdős problems site has stopped accepting AI-generated proofs that come without explanation. It has also stopped tallying the number of problems solved, shifting to favor human-readable write-ups linked to Lean proofs. Ben Antieau's Hexagon accepts LLM-assisted results without requiring formal verification, but limits the number of submissions in return. Both are answers to the question of how to allocate trust in the face of a flood of output. Hales's proposal can be seen as shoring up the "machine verification" side of that.

To make OpenAI's claims truly credible, it would need to show at least the following: a list of the axioms each formalized theorem depends on, along with proof that sorry and native_decide were not used; the results of rechecking the proofs with a checker implemented independently of Lean's official kernel; a record of human experts confirming that the formalized statements match the papers' claims; and which model produced the results, under what conditions.

Until those are in place, "about 42% is formalized" does not mean "42% is guaranteed to be correct." It means only that "42% was accepted by a single verifier that has not itself been fully verified." If the change AI brings to mathematics is the big deal Zvi says it is, then the word "verified" underneath it deserves to be scrutinized with the same intensity as the results themselves.