r/math • u/Carl_LaFong • 19h ago
Trust Lean proof?
I see many people claiming you can’t trust a Lean proof because Lean is buggy. I know someone tried to validate a false proof of Collatz by exploiting a bug. I also know that if there is an error in the Lean statements of the theorem or the axioms, the proof will be invalid. Is there any example of a false proof due to a bug or a reason other than the above?
22
u/Scrub_Spinifex 3h ago
I would absolutely 100% trust a LEAN proof written by mathematicians. Because what LEAN is actually doing is forcing you to detail your proof up to the most formal level. Which means that if there's a mistake in your proof, you'd realize it in the process. And you wouldn't exploit a bug by accident, because those bugs don't correspond to ways of deduction that mathematically make sense. The only situation when a mathematician could write a fake LEAN proof exploiting a bug is if they're deliberately attempting to scam the community (or to bring the bug to light, as was IIRC the case for the fake Collatz proof).
I'd not 100% trust a LEAN proof written by an AI. Because an AI doesn't necessarily have the same goals as mathematicians. If the prompt is "write a proof that compiles", it may just try to scam its way to this task. And maybe to hide the use of the bug in a way that's particularly difficult to detect, or hide particularly well that the formalized statement of the theorem doesn't correspond to its human-language counterpart. In short, I trust my fellow mathematicians not to try to scam, me but I don't trust AIs for this.
However, I'd (say, 98%) trust an AI-formalized proof to be correct provided I asked to another agent to check it with the prompt "check the formalized statement correspond to its natural language counterpart and that the proof doesn't exploit bugs or introduce unwanted axioms". Especially if the agent is powered by a concurrent AI company (like, ask Claude to check a GPT proof). The remaining 2% are for the case when the agent writing the proof tried to scam its way and was very very good at hiding evidence, enough for the other agent not to detect it.
19
u/bonebranch 5h ago
Of course, stating that Lean proofs are buggy and not to be trusted is an exaggeration. Humans make all sorts of mistakes and oversights. In my area there are pretty well-known errors that most of the experts know about and just warn unsuspecting mathematicians using these papers for reference, and I myself have been burned by a paper that may not have been scrutinized as well as it should have been (at least one of the lemmas was false without additional hypotheses, and even with the added assumptions my advisor and I could not get the claimed conclusion).
A proof that is properly formalized in Lean should be much, much more trustworthy than a purely natural language proof. That still has to be checked. Especially being that LLMs are known to do all sorts of things to achieve a task, even things that are potentially underhanded/illegal/dangerous.
I will also say that there are cranks and slop merchants who attach Lean files to bolster their papers, even if a cursory look at the human-written part of the text causes the whole thing to fall apart. Take your pick of claim to solution to favorite unsolved problem from ArXiV/Vixra/Zenodo/Hexagon, look for an attached Lean file and you'll quickly see that the mere existence of Lean code is no guarantee of correctness.
28
u/apnorton 6h ago
Lean is not a formally verified piece of software. The Lean kernel has had bugs in it in the past that allowed the "proof" of statements regardless of truth value. (The Collatz case you mention is one such example.) While the Lean kernel is quite rigorously tested, there's no proof that another such bug does not exist.
The simplest way to have an invalid Lean proof, which was far more common before people were using LLMs to generate Lean scaffolding code from the ground up, was by using the sorry instruction to assume their conclusion in a way they didn't realize. Now that it's a lot rarer to encounter a sorry at all, this class of error has all but died out.
11
u/NullOfSpace 5h ago
You can also check automatically whether a given Lean proof relies (directly or indirectly) on a given axiom, most notably sorryAx (which is what lets you use sorry as a statement).
4
u/satanic_satanist 4h ago
There are formally verified reimplementations of the Lean kernel, conLeche for example
4
u/backyard_tractorbeam 2h ago
I mean, the right response is probably to have patience and look closely at con-leche, but
The checker is practically useful and has good performance. I consider it production ready.
It was implemented and proven to be consistent by Claude (Fable and Opus), under heavy supervision by Joachim Breitner at the Lean FRO. See the git history for all the detours and dead ends it took.
This README is actually human written (with AI only doing copy-editing, fact checking and filling in numbers). It is probably the only human written thing in this repository.
I would vastly prefer if the con-leche author had at least written, personally, a paper about this consistent lean checker.
28
u/FantaSeahorse 6h ago
Yes Lean can have bugs. There could even be bugs in the C++ compiler which is used in the compilation of Lean itself. Cosmic rays can randomly flip the bits in the computers used for checking Lean proofs, etc. It’s impossible to have 100% guarantee in the correctness of software.
However, it’s still much more reliable than natural language proofs as they have been checked so far in human history. I think most mathematicians who have an understanding of how Lean (or in general proof assistants) works will tell you that. As a loose analogy, would you trust a computer or a human on multiplying two 1000 by 1000 matrices?
In the field of programming language theory, for example, having mechanized (computer-checked) proofs for theorems is increasingly valued by the peer review process.
If someone doesn’t trust Lean-verified proofs (after making sure the theorem statements and definitions match), then I don’t see how they can justify trusting human-verified ones
→ More replies (1)25
u/apnorton 5h ago
If someone doesn’t trust Lean-verified proofs (after making sure the theorem statements and definitions match), then I don’t see how they can justify trusting human-verified ones
I trust a Lean proof when a human writes it. However, my worry/distrust creeps in when dealing with thousands of lines of unreviewed, AI generated code that make up the Lean proof. Just like how the hypothetical Paperclipper sacrifices humanity in pursuit of more paperclips --- if you task an AI to "generate compiling Lean proof," it may very well realize that obfuscating a kernel exploit is far more efficient of a route to getting a compiling project than generating an actual proof.
I mostly trust a human to not deliberately try to deceive the reader and obfuscate a kernel bug --- after all, if the proof was something a human could fit in their mental context to write, it won't be outside of the realm of possibility to have a human check it, and intentional deception would result in grievous reputational harm to the human researcher... but an AI can a) easily generate more code than could ever be checked by a human, and b) has no notion of reputational harm caused by deceiving its users.
I do view AI generated Lean proofs as exceedingly high evidence that a claim is true, but until the proof is understood by a human, I don't find myself willing to accept it on its own.
This is kind of a variation on the view that many have to the controversial work on the ABC conjecture --- it could very well be true, but until the proof is something we can understand, then it's not really going to get widespread acceptance.
→ More replies (1)12
u/FantaSeahorse 5h ago
I definitely agree a human needs to review the Lean theorems and at least some of the proofs, but there is quite a bit of grey area in defining how much checking is enough.
In paper proofs it’s very common to hand wave when it comes to stuff like “treating isomorphic objects as equal”, “apply analogous arguments to other cases”, “w.l.o.g”, etc. Proof assistants will have to spell all of that out explicitly. I would argue that requiring humans to read through ALL mechanized proofs is counterproductive and usually just impossible. Reading thru statements of key lemmas and how they are used in the theorem is more reasonable imo.
About the idea that AI can take shortcuts by exploiting software bugs and not revealing it.. it’s definitely a real concern but one could equally incentivize another AI to check that no such shenanigans are happening. Ultimately it’s impossible to know for sure.
But again, I am arguing that Lean + human expert is more reliable than human expert alone, not that we don’t need human experts, so I don’t think we are disagreeing much
→ More replies (1)
5
u/Smart-Button-3221 2h ago
Lean is more trustworthy than proofs written on paper.
There's still ways to cheat both, and AI are particularly good at cheating.
8
u/Smallpaul 6h ago
If is not true that Lean is buggy. Lean is far more reliable than most software and has many levels of validation and safety. Bugs could still exist but practically speaking they are inconsequential.
I have been involved in this debate dozens of times on Reddit and nobody has once pointed me to a proof that was formalized in Lean and then later proven to be false either due to a bug or even just to a misformalization of the problem definition. Empirically, encoding in Lean should give one much more confidence than having ten mathematicians read the proof.
And in fact Peter Scholtze, mathematical superstar, asked Kevin Buzzard to formalize parts of one of his proofs because he wanted to be sure it was correct. Empirically speaking: encoding in Lean is how you get much higher confidence that it is correct. Because human reviewers are only human. We make mistakes.
10
u/apnorton 6h ago
Bugs could still exist but practically speaking they are inconsequential. (...) nobody has once pointed me to a proof that was formalized in Lean and then later proven to be false either due to a bug (...)
You mean like this one? https://infosec.exchange/@0xabad1dea/117002106099986943
18
u/InternetMandate 5h ago edited 5h ago
I think there’s an important distinction here. The Collatz case wasn’t an ordinary mathematical proof with a subtle error that Lean failed to catch. It involved exploiting a bug in Lean’s kernel to make it accept invalid proofs. That’s a very different failure mode.
If we’re considering deliberately adversarial attempts to defeat verification, we should apply the same standard to human-reviewed mathematics. As someone who writes mathematical proofs professionally, I can assure you it would be quite easy to introduce subtle errors into sufficiently complicated arguments if I were actively trying to deceive reviewers. And at least in my field, proofs are already cumbersome enough to check without anyone deliberately making them worse.
Meanwhile, ordinary mathematical errors do get through peer review. For example, Bayraktar and Guo published a strong equivalence result for Wasserstein metrics in Electronic Communications in Probability, a reputable probability journal, in 2021. In 2025, they published an erratum acknowledging errors and substantially weakening their conclusions.
That’s four years between publication and formal correction of a significant mathematical claim. Having a computer check the original argument would have been rather useful.
Kernel bugs are obviously serious, but a deliberately engineered exploit isn’t particularly informative about the relative reliability of Lean verification and ordinary mathematical peer review.
13
u/Smallpaul 6h ago
That was a targeted attack by an expert in proof software. Not a legitimate attempt to prove anything.
From your link:
“IMPORTANT EDIT: it was later clarified that the person who originally posted the proof was already aware that it was buggy, and chose not to be clear about this up front, as a humorous way to file a bug.”
4
→ More replies (1)2
u/qualiaisbackagain 5h ago
Misformalization, missing assumptions, and loose statements are still a problem. Theres a good case of this discussed in the AI4SLT paper. Theres a couple of Erdos problems that have also suffered from this. Im sure AI will get better at this, but it is difficult to feel comfortable fully trusting it without at least some human review.
→ More replies (2)
1
u/klexomat3000 4h ago
I've found this post from Thomas Hales on the matter insightful. I'm quoting part of it, but the whole text is worth reading.
Ken Thompson famously wrote “Reflections on Trusting Trust”. He asked, “To what extent should one trust a statement that a program is free of Trojan horses?” He imagines malicious code that finds its way into compilers and hides its own presence. His conclusion is, “You can’t trust code that you did not totally create yourself… No amount of source-level verification or scrutiny will protect you from using untrusted code.”
Today, in the age of AI, which increasingly has the capability to deceive us and to exploit software vulnerabilities, we absolutely cannot put blind trust in systems such as Lean. Taking an adversarial view of AI, we might ask how to certify that AI did not leave a backdoor soundness bug in Lean when it did its sweep for bugs in the summer of 2026? What if the bug is so obscure that humans are very unlikely to find it on their own? What if that very bug was exploited in the Lean verification of the Con-Leche checker, leaving a soundness bug in Con-Leche too? (Now that Con-Leche’s consistency has been cross-checked by multiple other kernels, a soundness bug would have to defeat all these cross-checks as well.) Then suppose that bug is used maliciously to plant a backdoor in formally verified software that protects critical infrastructure. What precautions do we take now to prevent this type of future scenario? During the past year, much foundational work on the type-theoretic foundations of math and its reliability has been relegated to AI, and this is dangerous unless carefully audited by humans.
1
u/parkway_parkway 3h ago
This is a classic problem in formal mathematics. You can only trust a proof checker as much as you trust its code.
Metamath has a really good solution to this.
Firstly all steps of the proof are completely explicit and so everything can be viewed whereas in lean there are automated tactics which hide things.
Secondly there are seven different verifiers written in seven different programming languages that are run on the database to check it.
So it's extremely unlikely all of them contain the same bug.
If you trust the theoretical model behind the proof checker which is extremely simple then there's enough implementations to really trust that it is working correctly.
1
u/SwimmerOld6155 3h ago edited 3h ago
from my understanding all the soundness bugs are very contrived and impossible to stumble on accidentally. someone didn't try to validate a false proof of Collatz, they found a soundness bug and announced a proof of Collatz as a joke basically.
It is possible that a misaligned AI could exploit a bug in a proof. I think it's unlikely and that independent review by subagents would circumvent this, but it is a possibility that should be minded. But when writing a Lean proof, it seems a general-purpose LLM's goal is not just to pass the compiler, it will actively look for sorrys and such. If you trained an LLM just to pass the compiler and nothing else, it'd be much more of a possibility.
1
1
u/Fancy-Jackfruit8578 55m ago
Do you trust humans to read proofs? Seriously, with the amount of papers published each day, something must be wrong too, but we are just believing that because a human has reviewed it.
1
100
u/Upbeat_Assist2680 6h ago
Lean is a complex bit of software and we expect implementation errors to be there and arise periodically. These are not, however, issues with the fundamental principle of the system as a proof assistant.
Other issues that arise -- especially with AI generated proofs -- is the possibility of an incorrect definition or theorem statement being introduced. Lean is a formal language and formulating complex concepts in the language is not always obvious.
I don't have specific examples.