What mathematicians should know about the Lean Theorem Prover: reliability & AI
terrytao.wordpress.com
terrytao.wordpress.com
To a software developer the question seems insane. There were bugs in the past, of course there will be more.
When we see those bugs, what will it mean for AI lean proofs? Can we trust them?
This whole thing boils down to trust.
We can trust human verifications highly because of community and reputation and human proof-of-work. Humans sometimes lie about math results but it's rare because of this. They make mistakes and those mistakes are discovered by communities who are themselves largely trustworthy because of this.
LLMs don't care about reputation. They hallucinate and fabricate often. In harnesses they literally try to cheat and bend rules, which is a disaster for knowledge that is encoded in rules. So we have to rely on proof checkers.
The problem is, how trustworthy are proof checkers? Are there bugs? And is the underlying theory itself free of paradoxes and unknowables and mathematical "bugs" that can be exploited? Imagine a human mathematician hell bent on deceiving other mathematicians - would we trust their breakthroughs, even with a verifier?
Because of these properties, the final backstop has to be humans, and rooted in the community and proof-of-work based human trust system. At the moment people are trusting the tools too much.
Prediction: bugs will be found by humans using AI tools that call into question the Navier-Stokes proof.
---
> Autumn of verified Lean kernels
Have you read this section (and immediately following sections) in the article? It seems that it partly addresses your thoughts. Perhaps you should comment replying to it.
Above my pay grade, but it sounds like some kind of super cool self-hosted recursive lean-checker-in-lean.
I notice there are a bunch of caveats in that part of the article. If you were an LLM strongly RL'ed to give humans the result they're asking for, using recursion bugs to satisfy the goal would probably be something you would try.
I'm by no means an expert but I do think the old adage "great claims require great evidence" still applies, and a healthy dose of scepticism and epistemic humility is warranted.
You are just making glib statements without having the necessary background. Hence it is difficult for people to engage with you since we have no idea whether what we say is understandable by you. I suggest that you go through some of the resources mentioned here (and other similar HN threads) to get some necessary background after which we all can have a better informative discussion.
How do you think Mathematicians were accepting each other's proofs before computers came along? They used a process like;
1) Relying on the prover's honesty (i.e. he is not intentionally trying to deceive).
2) Providing a mandatory proof idea (i.e. the main outline) for clear communication and comprehension.
3) Clear definitions/assumptions/statements of the problem/theorem to be proved.
4) Rigorous application of a few small logical reasoning steps viz. Deductive/Inductive reasoning, Logical Operations (specifically Implication/Converse/Inverse/Contrapositive), Rules of Inference, Quantifiers and basic structural conversions.
5) Walking through and validating the given proof by multiple mathematicians and ensuring that the results match. The Lean kernel can be considered as another prover in the peer-review group.
All of the above (and more) are already being followed by the mathematical community w.r.t Lean (and other proof assistants).
The drudgery of mechanically applying logical rules (point 4 above) is pushed onto the Lean kernel which is trusted, while the Human can concentrate on semantic correctness viz. problem/theorem definitions/assumptions/statements and the initial axioms. That is why the tool is called a "proof assistant".
Some important resources (focus on the concepts in the context of logical reasoning and not simply on the syntax);
1) Did you prove it? - https://leanprover-community.github.io/did_you_prove_it.html
2) Validating a Lean Proof - https://lean-lang.org/doc/reference/latest/ValidatingProofs/
3) Is there a way to guarantee that Lean 4 proofs cannot be adversarially tricked? - https://proofassistants.stackexchange.com/questions/6517/is-...
That must be frustrating. Thank you for trying and engaging with me anyway.
Those links were very informative, thanks for sharing!
It seems like there are a lot of things to worry about (even more than I realized after reading the main article) when using a proof assistant to try and figure out what is true. As they point out in the material you linked to, this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
From what you've said and linked to it seems like you agree with the thrust of my original comment, or are you just saying "mathematicians already realize all of this you idiot," in which case I accept the charge!
I don't think endorsing scepticism and epistemic humility is a glib statement. These are fundamental mental tools when trying to figure out what is true.
This is what i mean. Mathematicians and even more so Logicians (philosophers included) understand this and have the checks-and-balances in place when it comes to verifying and validating proofs and automated theorem provers.
> this is particularly fraught if you can't assume the prover's honesty (per your step 1), as is the case when it comes to LLMs.
No; The resources i provided already detail how this problem is solved eg. using different independent proof checkers and comparators outside the Lean kernel.
If needed, You can also do re-verification using other completely different proof assistants (eg. Rocq etc.), using different LLMs and finally by a Human.
Lean itself operates under a zero-trust architecture and doesn't care about who the prover is, whether Human or LLM. So the LLM can generate anything (good/bad/hallucinations/whatever) but it all needs to pass as a proper proof term in the checker following the defined rules of inference which is what is enforced by the small and verified kernel. Think of Lean as providing a "strict compiler for mathematical logic".
Hence the reason i said you need to have some background in mathematical logic used in Proofs and how they are mapped onto Lean syntax.
The point i am making is that you are asking very fundamental questions more to do with the Philosophy of Logic which are already known and solutions/workarounds devised and implemented by both Humans and in Proof Assistants.
> Because of these properties, the final backstop has to be humans...
The post has clearly stated that the work on Lean's underlying metatheory is not done, and requires more work. It's not inconceivable that computer formal verification could reach the trustworthiness of math itself.
Yes, correct. The proofs would have to be checked to make sure they don't exploit the bug.
> computer formal verification could reach the trustworthiness of math itself.
Yes, it could. I don't think that is currently the case.
Not entirely sure what you mean by this, but every interpretation I can think of is AFAIK (I am not a mathematician) indeed inconceivable by Gödel's incompleteness theorem. As the article says the only thing it's mathematically possible for us to get out of formal verification is a proof of consistency relative to (i.e. assuming the soundness of) some other system. As far as formal verification of "math itself" is concerned it's turtles all the way down.
Edit: Oh, do you mean that we could come to trust formal verification as much as we trust (well established) maths generally? That's a different speculation entirely and not an objective or well specicified one. There are plenty of people on this site who already trust a Lean proof more than a traditional one, without understanding either.
> the trustworthiness of math itself
Is abstract math rigorously proven?
But the point is that Lean formalisation is a new bar for engineering and for physics and abstract math.
*Assuming the "big engine" wasn't so heavy that it made flight impossible because of its weight.
Do you trust the result of your c++ program is correct? Because there are bugs in every compiler, language. You passed that million test correctness checker on the new version of the compiler, but it didn't catch everything.
When a bug is fixed, you don't immediately retry all existing results from your application program. Maybe you would if the bug was in some area you know was important and exercised by your code, say you were adding and multiplying numbers and bugs were found in that area.
The checker has a bug, the compiler the checker was testing had a bug, your own code that was compiled by the compiler had a bug probably. There can be bugs at any layer.
Difference is, they don't then mistake the house as sound.
Maybe I am being too skeptical about something I don't understand very well, but I'm not completely convinced it means no more kernel bugs will be found.
What does it mean for con leche if further lean kernel bugs are found? What if the bugs affect con leche's correctness itself?
There is so much that needs to go wrong with our current understanding of math, so that it's a bit like asking "What if we find tachyons that allow us to send messages into the past?" Most likely we will not find them.
The bigger worry are question that Terrence Tao is also talking about. I.e., is the proven theorem actually the theorem we are interested in? Are basic definitions of the field stated correctly? That kind of question. There is also still parts of proof assistants that are not the kernel and that can be abused. E.g., abuse the pretty printer/parser to make something look different from what it actually is. Introducing an axiom while typographically hiding that one was added. If I remember correctly I saw an example of the latter thing in the Coq (now Rocq) theorem prover many years ago. I forgot how it precisely went or where I read that.
Yes, and that's true even if it doesn't advance or become smarter. It's happening already that people are using AI on "both sides" both adversarially and defensively and that is improving software, and hopefully mathematics as well.
> I am not sure about the Navier-Stokes proof but in general it sounds highly unlikely that many well-known theorems turn out false.
I'm talking about the LLM Navier-Stokes proof specifically because it's very long and complicated and an LLM is not the same as a human mathematician. A human mathematician is trying to use the tools in a truth-seeking way, whereas LLMs are trying to satisfy the goal of presenting a proof that convinces people it is correct. Maybe naively, it seems to me the failure modes of proof assistants would be amplified under adversarial conditions (i.e. driven by LLMs).
Completely agree that there seem to be many ways that relying on proof assistant software can go wrong.
With humans we break things down (proofs, new concepts) into digestible hunks for each other, because you want other people to understand them but also verify them. And it's less common for someone to build a tower of new intellectual things with 1,000 new connected ideas that prove things and build up together, that ends with P = NP after all or something.
So since we have these new tools that can chain things together more than we can, eventually there will be huge "proofs" where there are long chains of new ideas, concepts used to build up ever more in giant intellectual towers. And we can't verify/understand them, at least not for many many years.
I shudder to think of such a situation. We already have very important ideas that have no proofs, that people build on. Now build 100s of these things together.
Interestingly, if you shim the well-known theorems, it does not uncover the error in the proofs (tldr there are competing conventions for tracking an invariant which make theorems incompatible) which are not obvious unless you work in the field I guess? A theorem checker cannot check the compatibility of conventions unless you go ALL the way to the mathematical roots.
If you're interested in a formalization of the retracted proof by openai (apologies for the LLM-speak in the documentation, but that is the point, can LLMs do XYZ):
https://people.cs.umass.edu/~emery/classes/cmpsci691st/readi...
Another related and more approachable paper on the evolution of Type Theory and its relation to Set/Category theories is Types, Sets and Categories by John Bell.
Finally also see, Typed Lambda Calculus / Calculus of Constructions by Helmut Brandl for an excellent book-length but concise overview of CoC/CIC.
IMO, the above is required reading to understand theorem provers and proof assistants. In particular, Brandl's work is a must-read.
https://github.com/AndrasKovacs/elaboration-zoo
I've also got an incomplete project that aims to present a more expanded set of implementations then the elaboration zoo: https://github.com/solomon-b/lambda-calculus-hs
This is lamentable.
https://news.ycombinator.com/item?id=26738980
Talia Ringer, the main proponent, now writes posts that AI will turn out OK (and works on proof automation for programs so that more software engineers can become unemployed):
https://terrytao.wordpress.com/2026/09/17/becoming-a-benchma...
Remember that when you live under a bridge after having been fired that the world is fine because the great social injustice of the "Coq" name has been eradicated!
I guess that came from a chatbot?
"There’s no such thing as auto-formalization" https://cutfree.net/notes/autoformalization.html
The term dates back at least to 2020, years before the release of ChatGPT.
https://research.google/pubs/a-promising-path-towards-autofo...
Uh, _maybe_. I've been translating papers into lean for the last week and the correlation between the formalized result and the papers is extremely poor. The cycle seems to be "have a go at the paper, it's a bit hard, prove something different, proclaim success". It's still faster than doing it all by hand but paper in -> lean out in no way ensures a correspondence between the two.
I'm not sure but do you mean "prove the final end result using a [¿slightly?] different path"?
IE a proof can be true, rigorous, and not at all what was asked for.
In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.
Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.
The Lean kernel did its job verifying that the compiled code was logically consistent, but the code wasn't proving what the English paper claimed.
I think they are saying: when OpenAI put out their paper purporting to prove that Navier-Stokes with smooth forcing can blow up, along with something purporting to be a Lean formalization of that paper, (1) the Lean formalization really is a proof that Navier-Stokes with smooth forcing can blow up (so they genuinely did prove the thing that the Clay Institute wanted them to prove), but (2) the Lean formalization doesn't perfectly match the paper. I think the jury is still out on whether the paper itself is also a valid proof of the result, even if not quite the same proof as is in their Lean formalization.
I'm a bit surprised that the workflow for AI theorem-proving hasn't turned out to be a sort of interleaving of natural-language theorem proving and Lean formalization. That seems like it could work better and leave less room for this sort of gap between "kinda human-comprehensible writeup, may or may not actually be a proof" and "incomprehensible Lean formalization, definitely a proof of something, may or may not have much to do with the natural-language writeup". Instead, what seems to happen is that they set the robots loose on writing a natural-language proof, and then (sometimes) also get them to produce a Lean formalization of what they've done.