Lean 验证为何不等于证明正确：AI 时代数学证明的可信度问题

This will probably be the first in a series of posts on the current state of mathematics and its future given what AI can now do. I want it to be a reasonably instructive account of when and how much one should value the now omnipresent “verified in Lean” and also to write down some less factual personal beliefs.

In June I got to spend a few days in the Colorado mountains in exchange for giving a talk about a computational formalization of flag algebras in Lean.¹ It is not a forgiving topic to present, because both formal proof verification and flag algebras are tools that people are often eager to use but not so eager to understand. After the mandatory too-terse-to-be-useful introduction to Lean, I got a question similar to this:

“So if someone submits a paper and claims that it is fully verified in Lean, how do I as an editor know that this actually means the paper is correct?”

This was before Fable and Astra were publicly released, but Erdős’s unit distance conjecture had already been disproven by “an internal model” of OpenAI just two weeks earlier. The evening of my talk was also the first time I saw four tenured professors standing at a blackboard at 10pm, scratching their heads, trying to decide whether to believe a proof that “it” had come up with for a problem they were working on. So while the question was not one my talk was meant to answer, it is probably one that deserves at least an attempt at an answer.

There is a technical and factually correct answer as to when Lean code might not actually serve as a certificate of a proof. Your favorite AI chat platform will probably give you something similar to the following list, which I wrote down for the last iteration of my Lean course:

1. The relevant part is not formalized. A curious example comes out of OpenAI’s proof that the chromatic number of the plane is at least 6: in a footnote, it is briefly mentioned that a manuscript had already claimed it to be 7 with allusions to a formal verification in Lean; however, that formal verification addresses only part of the claimed proof. Its main formal theorem assumes a bound on the angular measure of unit-distance-free subsets of the unit circle – a bound that, as OpenAI’s internal model notes, does not hold. In other words, an LLM correctly fact-checked a human-written paper that advertised a Lean certificate.

2. The formal proof differs from the written proof. Bastounis, Circelli and Hansen found that several intermediate estimates in the Lean code accompanying OpenAI’s proof of blow-up for Navier–Stokes require one more derivative than the corresponding estimates in the written paper. The theorem is verified but, strictly speaking, the proof in that paper is not.

3. The formal statement differs from the intended one. For years, the published Coq formalization of the irrationality of \(\zeta(3)\) stated its main theorem with = instead of ==. The erroneous statement merely said the partial-sum sequence was not constant; it did not establish that its limit was irrational. The proof itself was fine.

4. The proof has gaps or relies on additional axioms. A sorry leaves a step unproved and an axiom simply asserts one beyond the three standard ones (propext, Classical.choice, Quot.sound). A more subtle variant is native_decide, which trusts compiled code instead of the kernel. All of these are flagged, but the warnings can be switched off with a simple set_option.

5. A kernel bug is exploited. In July, a “disproof” of the Collatz conjecture compiled without sorry or additional axioms because it exploited a bug in the kernel’s handling of nested inductive types.²

6. The compiler chain or hardware has a trust issue. The kernel is itself a compiled program, so one ultimately trusts every compiler in that chain, as well as the hardware it runs on.

These are all correct and relevant, but I believe they don’t really answer the question. To some, editors in particular, the promise of formal verification was that you no longer need to think about a proof to trust it; but the points above show that it just shifts what you have to think about.

The actual answer is sadly non-technical and unsatisfying: Lean code is speech, and speech can be used to both inform and misinform. As a formal language, Lean imposes strong constraints that make it significantly harder to do the latter, but it ultimately cannot prevent it – in particular when the misinformation lives at the interface to natural language. At the same time, the constraints increase the recipient’s belief that the information is correct, which can make misuse, whether with malice or negligence,³ more likely to occur.

If I had to give an actual pragmatic answer, it would be that Lean code only makes sense for the purpose of certification if at least three things are checked by someone sufficiently knowledgeable:

1. The statements for which verification is claimed are actually the statements being verified in code.
2. The code builds on community-accepted definitions and statements, and ideally the statements and definitions not come from the same people who provide the proof. If that is not the case, at least the final statement, its assumptions, and the definitions needed for it must be reviewed.
3. There are no signs of abusing or misusing the system: no added axiom (checked with #print axioms), no leftover sorry, no disabled linter warnings about unsafe operations, and nothing that looks like exploiting a kernel bug. Ideally, it compiles with up-to-date versions of Lean and Mathlib.

In most cases this is significantly easier than fully digesting a handwritten proof, but it is not trivial. Importantly, if you are asking this question, you most likely already have some reason to distrust the source of the result or the Lean certificate. No one doubts that the Liquid Tensor Experiment really formalized and verified the work of Clausen and Scholze because it was an openly communicated project and a collaboration between mathematicians with the genuine goal of removing the last bit of doubt about whether a black-box result, whose proof very few will ever fully read or digest but which will be used downstream, really holds.

The same cannot be said of the avalanche of AI-generated proofs that all come with the seal “verified in Lean”. If the reason for including Lean code is that the authors did not even digest the proof well enough to feel comfortable putting their name on it, then serving it with equally unread Lean code, to me, reduces trust rather than increasing it. Cheap formalization weakens the signal of human engagement, even when the certificate remains mathematically valid. Phrased more constructively: if you have read the proof, judged it sound, and written up an exposition in your own words, asking an LLM for Lean code that no one will read adds little.

To be clear, this does not mean that I believe OpenAI’s dump of 700+ papers, many of which are breakthroughs by most measures, to be incorrect. On the contrary, my faith in the ability of the latest LLMs to detect flaws in mathematical arguments, even without any Lean verification, has drastically increased in the last few months to the point where some critical probing with an LLM fulfills most of the promises of a ‘verified in Lean’ stamp. It is also quite possible that formal proof verification plays an important role for the big AI labs in getting to that point, i.e., in deciding which signal to reinforce during the training. But that is a different question and of less relevance to mathematicians not working in machine learning and the training or evaluation of these networks.

To end on a slightly more cheerful note: just as the value of a proof was never only that it settles a statement, the value of formal code was never only the certificate. Ideally it also helps those who write or read it to understand a proof through a more rigorous and unforgiving structure. Contributing to Mathlib also means discussing with others and reaching a consensus on definitions, statements, and proofs – a much more invasive process than publishing a paper. At least for me, working with Lean has significantly shaped how I think about math and its foundations, and I am thankful for that.

1. The goal is basically to allow one to write down any flag algebra (in)equality (sum-of-squares or other) and have Lean verify and connect it to actual statements in graph theory. I should note that Gyeongwon Jeong, Seonghun Park, Jihoon Hyun, Sang-il Oum and Hongseok Yang also independently formalized flag algebras in Lean and (unlike me) already made their code available. ↩

2. It also passed an independent checker by exploiting a separate bug. The kernel bug was fixed within an hour of being reported and the bug in the independent checker had already been fixed, but the check was run with an outdated version. ↩

3. One can certainly imagine a mathematician subconsciously turning a blind eye to an issue in their definitions because it makes a proof work and while it may be less plausible for them to act maliciously, thousands of agents trapped in a box with an impossible task just might. ↩