6 ms·
> 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 tha
by FartyMcFarter 11d 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 11d 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.
- tsimionescu 11d agoThat's a completely different matter than what this thread was about. This thread was about whether mistakes in the 13M lines of Lean code could mean that this proof could be wrong despite Lean saying it's right.