Hacker News Reader

Comment by voidhorse | Hacker News Reader

To 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.

View on HN

Fortunately FLT is an extremely simple statement. Much easier to satisfy yourself that its statement is what you wanted to say than it would be for most statements of interest!

From 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.

No expertise at all on interactive theorem provers like Lean but I am familiar with Resolution-based automated theorem proving. In that setting, one writes down a theory, in the form of a set of first-order definite program clauses, and then presents a statement to the prover, then the prover proceeds to prove the statement is a theorem derived from the theory.

Is that (other than the language not being definite logic) more or less what Lean does also? In that case, isn't all the work in writing down the theory, and isn't that the step where mistakes can creep in?

Is that more or less what you're pointing out? That FLT is simple enough to state but the theory from which it is to be derived can be mangled and so accept FLT on the wrong grounds?

> 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.

But 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.

That'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.

Reply on news.ycombinator.com