3 ms·
So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering back
by herbcso 28d ago
So I don't know Lean or Mathematics to any degree to really be able to say this with any level of confidence, but speaking from a pure software engineering backgrouand, how do we know that 13 MILLION lines of Lean code are bug-free? It seems to me that for a mathematical proof, bug-free would be an absolute requirement. Maybe the structure of Lean imposes that, I don't know, but that seems highly unlikely to me. That just feels like a LOT of code to be comletely error-free... What am I missing here?
- twiceaday 28d agoLean is like a statically typed programming language and validity is guaranteed if it compiles. The only room for errors is in translating a non-Lean theorem into Lean, so that you are not proving what you think you are proving.
- throw-qqqqq 28d agoGreat explanation. I’ve heard this referred to, as The Formal Specification problem. From https://en.wikipedia.org/wiki/Formal_specification#Limitations https://en.wikipedia.org/wiki/Formal_specification#Limitatio... > A design (or implementation) cannot ever be declared “correct” on its own. It can only ever be “correct with respect to a given specification.” Whether the formal specification correctly describes the problem to be solved is a separate issue.
- thevivekpandey 28d agoIn lean, a theorem is specified by a type (in their highly complex "dependent type system") and proof is specified by a code that produces a term of that type. If the compiler certifies that the code indeed produces a term of that type, then the proof is correct. So, only need to trust: (1) That theorem statement is correctly encoded (FLT has a very short 1 liner description really) (2) Lean compiler is correct
- gorgolo 28d ago> That theorem statement is correctly encoded (FLT has a very short 1 liner description really) As someone not very familiar with Lean, does it really just depend on the entry point / theorem being correctly encoded? Can intermediate statements ever be mis encoded or misinterpreted, or is this what would count as a “bug in the Lean compiler”?
- SkidanovAlex 28d agoIt is the latter. If you are certain your theorem is stated correctly, and you believe that the Lean kernel against which you validate is correct, your proof is correct. This is how the theorem for FLT looks in the particular proof we discuss here: theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n As long as this statement is correct, and the kernel is correct, the proof could be trillion lines of code, and if the kernel says it is correct, it is correct. This proof was checked against TWO independently built kernels. So you would need TWO kernels to have the same bug to mistakenly accept an incorrect proof. (Not impossible: such a bug indeed was recently discovered (and patched))
- YeGoblynQueenne 27d agoCouldn't the kernels have different bugs?
- thejokeisonme 27d agoYou emphasize TWO as of these kernels are so different.
- aureianimus 28d agoThere's no guarantee that the intermediate statements match the informal mathematical intermediate statements, but if there is a mismatch, then this has to be repaired elsewhere to yield a proof that passes the Comparator tool. Running this tool indeed reduces the correctness question to what the parent comment mentioned.
- raincole 28d ago
- thrance 28d agoAnd (3) the axioms are correctly encoded too.
- not-so-darkstar 28d agoWhat if the mathematical objects are not encoded "correctly"? For example, everyone knows that the natural numbers and simple data structures like lists or trees can be encoded with inductive types, but what about the new objects introduced by the proof?
- robotpepi 28d agothat's something a human needs to do, and it's non trivial, but it's a simple task compared to checking the correctness of the proof. in any case, most of the language is probably already defined in Lean and checked independently by many people.
- not-so-darkstar 28d agoI think the other commenters are right, as long as the statement of FLT is correct and no funny stuff is used (admitting theorems without proof or defining new axioms) then it doesn't matter what you used in the proof.
- raincole 28d agoThe answer is we don't really know [0]: > In 2026, AIs designed to spot bugs in software were directed at Lean, and found several loopholes which were then fixed. Perhaps related to this effort, a purported disproof of the Collatz conjecture was announced as verified in Lean. However, this proof was soon determined to rely on a bug in Lean, and once the bug was fixed the proof was found invalid However it's a bit different than the usual 'bugs' we encounter in normal software development. Lean is more like a type checker. If you can write a false proof in Lean then the bug is in Lean itself, not your code. In other words, Lean can have bugs, but the amount of code we need to check scales with Lean itself, not with the length of proof. Just like the chance that C compiler has bugs doesn't increase as we write more C code. So the 13M lines of code doesn't really matter here. [0]: https://en.wikipedia.org/wiki/Lean_(proof_assistant) https://en.wikipedia.org/wiki/Lean_(proof_assistant)
- dwohnitmok 28d agoThe structure of Lean does impose that. The code isn't being run, it's being type checked. And that's it. The overwhelming majority of Lean code is never run. It exists only to be type checked (because type checking is equivalent to verifying the proof). You could imagine the typechecker has bugs (and indeed another comment mentions examples of bugs!). Crucially though anytime the typechecker has a bug fixed you could rerun the typechecker on the code to see if it still type checks. This is the whole promise of formal verification. It reduces the problem of verification purely to the typechecker. If the typechecker is correct, then the proof is verified, no matter how many lines of code the proof is. As a sibling comment puts it, the chance of bugs mainly scales with the number of lines of code in the typechecker, not in the amount of lines of Lean code. Your question is akin to asking, "yes this spellchecker ran fine on your essay, but are you sure it runs fine on War and Peace? That's 1000x more words!" To which the answer is the number of words doesn't matter if the spell checker is correct (which it might not be! And longer passages might reveal more bugs! But you can always rerun it). The main source of bugs is more lines of code in the spell checker, not in number of words in the text.
- throw567643u8 28d agoWith the size of the proof object, a potential buffer overflow comes to mind.
- throw-qqqqq 28d agoBuffer overflows are trivial to check for at runtime (~proof-checking-time) and Lean does this. Just like Java does it. I’d wager a million gazillion bucks that this is not the case.
- throw567643u8 28d agoSo would you also say no chance of a stack overflow or any type of surreptitious storage overflow anywhere in the runtime do you think?
- FartyMcFarter 28d agoStack overflows are also trivial to check for, if one wants to. It's just comparing two pointers, plus checking for arithmetic overflow (in case the pointers run past the maximum value of the pointer type).
- throw-qqqqq 27d agoI would say it’s very unlikely to be the case here at least. Of course some bugs in Lean may exist (I don’t have deep insight into Lean’s implementation and there have been bugs before), but I find it unlikely to be systematical or in a format that could affect the proof. As I understand it, Lean is implemented in Lean and emits/compiles to C. In that C code, I’d be very surprised if any buffer overflows or stack overflows exist. Such overflows are not difficult or expensive to detect, so if any were there, it should cause a crash instead of an incorrect result. It’s not as in handwritten C where you can forget or omit a bounds check. I’d say it is even less likely than seeing an overflow in the Core of Java cause an incorrect result (i.e. corruption instead of a crash) - because Lean uses the De Bruijn principle of reducing to a very small Core, that is easier to keep correct (others in this thread have expanded on this I better than I can I think). Out of pure curiosity: Do you believe otherwise or have a reason to think I am mistaken?
- voidhorse 28d agoTo me, a lot of the child comments on this thread are technically correct (the best kind) in that, yes correctness bugs in Lean boil down to compiler bugs in a language like lean. What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode is still a major problem and yes, extremely difficult when you have that many lines to pore over. But, if you're using LLMs to vibe code millions of lines of "proof" you've already stopped caring about that and presumably given your critical reasoning and concern over to pure faith in machine gods anyway.
- latent-person 28d agoFrom the article: > The finished proof was checked by Lean; it uses just Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches Mathlib’s own statement of FLT. So it proved the statement of FLT made independently in Mathlib. So no reason to not trust it proved the correct thing.
- FartyMcFarter 28d ago> What these comments all miss is that ensuring your 13 million lines actually encode what you intend them to encode I don't think the comments are missing that at all. If the Lean compiler itself is bug-free, we can trust its verification of the 13 million lines of code. We don't need to verify them by hand. The encoding of the theorem itself needs to be trusted, as does the compiler. The proof doesn't need to be trusted, it gets checked by the compiler.
- SpicyLemonZest 27d agoBut what does it matter whether we can "trust its verification of the 13 million lines of code"? We already knew that Fermat's Last Theorem is true, we don't need Lean to tell us that. The value of a formalization would be to improve our understanding of why it's true, and that can't be achieved by 13 million lines of code no human being has read. The source article does acknowledge this isn't a replacement for human analysis, but they seem to imagine a vision of mathematical research where there's a bunch of AIs running around proving random things and formalizing them into opaque Lean proofs nobody ever has to read. I'm skeptical whether there's any value in doing that, and to the extent that there is I'm pretty confident it looks more like proving certain directions aren't fruitful for further investigation.