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.

FigureYes, this was generated with ChatGPT.

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 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 and even passed an independent checker, because it exploited a bug in the kernel’s handling of nested inductive types. The bug was fixed within an hour of being reported.
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 makes 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 statement of the central theorem does not come from the same people who provide the proof. If that is not the case, a proper review of all definitions and statements required for the main theorem is needed.
3. There are no signs of abusing or misusing the system: no added axiom, 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. Notably, all of this only becomes relevant if you do not have other reasons to trust 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 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 premise is that the authors did not even digest the proof well enough to put their name on it, then serving it with equally unread Lean code, to me, reduces trust rather than increasing it. Phrased more constructively: if you have read the proof and judge it sound, 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 has drastically increased in the last few months to the point where a Lean certificate just does not add much anymore.³

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. Instead, it ideally helps those who write or read it to understand a proof through a more rigorous and unforgiving structure. 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. 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. ↩

3. This is coming from the perspective of a mathematician consuming the end product. The big AI labs are unsurprisingly not very transparent about their training process, but I can imagine that mathematical problem solving is not just used for benchmarking after training has concluded, but that it plays an important role in the RL phase of training. It is quite possible that proof formalization is relevant for OpenAI to increase its trust in deciding which outputs to reinforce. ↩