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.
> 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?
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
Hidden like any subtle bug that one might gloss over when inspecting the source code. The statement you’re trying to prove could be thousands of lines long and that semantic mismatch could occur anywhere. We seem to be very blasé about this.
that's misunderstanding what lean does. It proves many statements of the form A implies C (I'll write this as A => C). If you chain many of these together, say A => B1 => B2 => ... => B500_000 => C, what you do is
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).
Okay this is more revealing, thank you. You’re saying that A and C are very small, humanly verifiable pieces of encoded logic. Can you give me an example of how Bs come into being and why they can never be wrong?
You might find The Hitchhiker's guide to reading Lean 4 Theorems useful - <a href="https://blog.lambdaclass.com/the-hitchhikers-guide-to-reading-lean-4-theorems/" rel="nofollow">https://blog.lambdaclass.com/the-hitchhikers-guide-to-readin...
Excerpt:
The Rosetta Stone
Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.
A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."
thom · · focus · HN ↗
thaumasiotes · · focus · HN ↗
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
thom · · focus · HN ↗
mswphd · · focus · HN ↗
1. examine A, and
2. examine C, and
3. rely on the Lean kernel to ensure that all of the interior transitions are correct.
Modulo a soundness bug in the lean kernel (which do occur), the entire proof is then correct, even if you only need to inspect the small fragments A and C to understand if this correct proof is interesting. But the semantics of the statements B1 ... B500_000 are irrelevant to the correctness of the final implication A => C (again, modulo soundness bugs in the lean kernel).
thom · · focus · HN ↗
rramadass · · focus · HN ↗
Excerpt:
The Rosetta Stone
Before diving into syntax, it helps to establish the translation between mathematical and programming concepts. Every idea in formal mathematics has a direct programming analogue.
A theorem is a function with a type signature. Its hypotheses are function parameters, and its conclusion is the return type. The proof is the function body — the implementation. A lemma is a helper function. ∀ (for all) is a generic type parameter. The arrow → means both "implies" and "function from A to B." Conjunction ∧ is a tuple. Disjunction ∨ is a tagged union. Existence ∃ is a dependent pair. Equality = is structural equality. And QED — the moment the kernel accepts the proof — is the moment the type checker says "this compiles."