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.
I think you misunderstand what a LEAN proof entails.
A statement corresponds to a type and to proof that statement means to show that this type is inhabitetd (i.e., there is actually a value of that type).
A proof is then "just a program" in "just a programming language". Crucially, you do not care what "this program computes" but you care only that the program actually has the given type.
There is no concept of a "bug" in a proof term because you do not actually care what a proof term "computes". You care that it exists and that it is well typed.
This might sound pedantic but it is worth being precise here. These kind of issues are either "Proving the wrong statements" or "using dubious axioms". Both of these are issues not issues of the proof. You do not need to understand the proof term to identify such issues nor do you need to understand the proof term to verify their absence.
I am not saying that LEAN proofs are without issues. What I am trying to say is that the proof term itself is not the trusted part.
To be convinced of a proof, an expert will have to (1) review the definitions, (2) review the axioms, and (3) trust the kernel.
Issues can arise in all 3 but the proof itself is untrusted.
Definitions in a formal language are hard and error prone. Axioms are mostly not an issue. Most LEAN proofs should only make use of the three standard axioms (Choice, Propext, and Quotient soundness) and it is well studied what these axioms mean. Actual bugs happen in 3. Kernel bugs can for example mean that the kernel incorrectly checks a proof of "False". Kernel bugs do happen but there are measures against it (e.g., using multiple kernels to check your proof) and it is quite rare for a human to accidentally trigger one. LLMs have accidentally triggered kernel bugs in the past.
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
thom · · focus · HN ↗
herni · · focus · HN ↗
A statement corresponds to a type and to proof that statement means to show that this type is inhabitetd (i.e., there is actually a value of that type).
A proof is then "just a program" in "just a programming language". Crucially, you do not care what "this program computes" but you care only that the program actually has the given type.
There is no concept of a "bug" in a proof term because you do not actually care what a proof term "computes". You care that it exists and that it is well typed.
thom · · focus · HN ↗
<a href="https://proceedings.mlr.press/v306/ammanamanchi26a.html" rel="nofollow">https://proceedings.mlr.press/v306/ammanamanchi26a.html
UltraSane · · focus · HN ↗
herni · · focus · HN ↗
I am not saying that LEAN proofs are without issues. What I am trying to say is that the proof term itself is not the trusted part.
To be convinced of a proof, an expert will have to (1) review the definitions, (2) review the axioms, and (3) trust the kernel.
Issues can arise in all 3 but the proof itself is untrusted.
Definitions in a formal language are hard and error prone. Axioms are mostly not an issue. Most LEAN proofs should only make use of the three standard axioms (Choice, Propext, and Quotient soundness) and it is well studied what these axioms mean. Actual bugs happen in 3. Kernel bugs can for example mean that the kernel incorrectly checks a proof of "False". Kernel bugs do happen but there are measures against it (e.g., using multiple kernels to check your proof) and it is quite rare for a human to accidentally trigger one. LLMs have accidentally triggered kernel bugs in the past.