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.
> inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless
In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
Because it won't type check. It's like asking how you know some function in a program really gets an Int argument when you had lots of data structures you were passing around with all kinds of fields with various names and types.
If you construct value of type `forall n, exists m, m≥n and m prime`, then you know you have such an object. Think of a `theorem` (the Lean keyword) as a function that returns such objects. If you try to return the wrong type (e.g. you build a `forall n, exists m, m≤n and m prime`) in your "function" body, you get a compile error. If you use types incorrectly in the middle (passing values and intermediate proofs to theorems incorrectly), you get a compile error.
It's just like any programming language except the type system is rich enough that in addition to being able to have a value x: Int, (so maybe x is 5) you can have values like h: x^2≥0 (so imagine h is some object you build that proves x^2≥0).
Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:
import Mathlib
abbrev Scalar := ℂ
abbrev Real := Scalar
theorem negative_one_has_a_real_square_root :
∃ x : Real, x * x = -1 := by
exact ⟨Complex.I, Complex.I_mul_I⟩
But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!
I think you're misreading Lean Web. Over on the right side with that you'll see:
`Real` has already been declared
for your `abbrev Real`, and you'll see
our
Application type mismatch: The argument
Complex.I
has type
ℂ
but is expected to have type
ℝ
in the application
Exists.intro Complex.I
for the first term in your `exact` brackets.
It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.
But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.
In a fixed version of your example, that means
- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`
- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
thom · · focus · HN ↗
SkiFire13 · · focus · HN ↗
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
thom · · focus · HN ↗
ndriscoll · · focus · HN ↗
If you construct value of type `forall n, exists m, m≥n and m prime`, then you know you have such an object. Think of a `theorem` (the Lean keyword) as a function that returns such objects. If you try to return the wrong type (e.g. you build a `forall n, exists m, m≤n and m prime`) in your "function" body, you get a compile error. If you use types incorrectly in the middle (passing values and intermediate proofs to theorems incorrectly), you get a compile error.
It's just like any programming language except the type system is rich enough that in addition to being able to have a value x: Int, (so maybe x is 5) you can have values like h: x^2≥0 (so imagine h is some object you build that proves x^2≥0).
thom · · focus · HN ↗
6gvONxR4sf7o · · focus · HN ↗
for the first term in your `exact` brackets.
It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.
But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.
In a fixed version of your example, that means
- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`
- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)
- it's not on you to understand the proof