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