So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
Much of the point is that you have to understand the lean statement, not its proof. If the proof checker says it's good and reports that it just uses the usual axioms, then you can trust that they imply the statement. And the statement is never the 500k line part.
How many new lines of Lean do these recent Millennium Prize proofs introduce on top of known good axioms? I suppose I’m asking what the actual workflow is to inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is, because I know of no other substantial source code produced by LLMs that has literally zero bugs, however strong the type system of the language it’s writing in.
The core of a proof checker is a formally validated core that is based on a small amount of concepts. Every single line in the proof reduces to that core, therefore, as long as you can trust the core, you can trust the execution of the proofs.
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
Yes but why do we write the last bit as an aside as if that’s not a massive yawning black hole for errors to hide in? All the other stuff is irrelevant, just like when Haskell and Rust people claim that if their code compiles it is correct.
Because in practice, it's very straightforward to check that all of the types for class members are what you expect. Especially when you actually use that class in other code. You have things in mind that the class should do. If you get compile errors doing those things, you notice the inconsistency.
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
thom · · focus · HN ↗
whateverboat · · focus · HN ↗
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
thom · · focus · HN ↗
ndriscoll · · focus · HN ↗