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.
There are things you can do in lean which are footguns. For example, 1/0 = 0 in lean. For much of math that's not a problem. Still though, you have to remember that this is the case for whatever number system you're doing a proof in. For things which map to real world scenarios it's potentially a big problem.
> Still though, you have to remember that this is the case for whatever number system you're doing a proof in.
This is generally untrue. The reason you don't have to remember is that your proof will inevitably rely on a theorem with "x ≠ 0" as one of the premises. (And if that doesn't happen, then the fact that lean defines division strangely isn't relevant to your proof.)
If what you're doing is writing code unaccompanied by proofs, then yes, this is something you'd have to remember.
> theorem with "x ≠ 0" as one of the premises
If you're writing that theorem: Assuming you remember to include it in your premises.
Sometimes the invariant might not be mathematical, it might be social. I recall a story where 1/0 caused a problem because stock issuance uses a 0-share disbursement as a tombstone: to indicate that "this stock account has zeroed out this security and has no remaining ownership". You might not have remembered that and you might have forgotten to record that as a necessary invariant in your proofs. If lean had defined division to have a nonzero denominator, it would have caught the problem even if you didn't know that a zero share disbursement hada a different meaning.
> If you're writing that theorem: Assuming you remember to include it in your premises.
No, you're missing the point. If you're writing that theorem, either (1) you will have to include that premise, and anyone who depends on you will have to satisfy it; or (2) the theorem is true regardless of what happens when you divide by zero, and nobody who depends on you will care. At no point can the division behavior hide something that comes back to bite you.
Mathlib includes theorems of both these types. For an example in a space I've been working with, you can compute the cardinality of a type with Nat.card. This returns a natural number, which is convenient, but since there is no infinitely large natural number, the value of Nat.card for an infinite set is 0.
If you care about the difference, you need ENat.card, which takes different values for empty and infinite types. But you usually won't want to do this, because the value of ENat.card is an extended natural rather than a natural, which makes it a huge pain to work with.
There are several theorems related to Nat.card which take advantage of the dummy "infinite" value of 0 to prove a theorem that is true regardless of what the cardinality might actually be, and omit any premise related to it (which would have taken the form "the type is finite", "the type is uninhabited", or "the type is infinite"). The advantage of doing things that way is that you don't have to detour into the extended naturals, and the validity of your proof is unaffected.
Consider Nat.card_prod, which says that
Nat.card (α × β) = Nat.card α * Nat.card β
When α and β are both finite, this says exactly what you'd expect.
In the case that α is infinite, Nat.card α will be zero, and therefore the product Nat.card α * Nat.card β will also be zero. It happens that when (α × β) is infinite, Nat.card (α × β) is zero (by definition), so this theorem is correct. The reasoning isn't something you'd want to repeat in those terms in an oral exam, but there are no mistakes, and the stated theorem is true.
> If lean had defined division to have a nonzero denominator
To write, for a human, yes. An LLM will happily write all the extra discharging statements needed.
However, to review, you have to hold the 1/0 = 0 in mind everywhere and propagate it everywhere, which is difficult for a human. If you had explicit discharging the human can easily remember "oh numbers work the way they ought to"
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.
dnautics · · focus · HN ↗
thaumasiotes · · focus · HN ↗
This is generally untrue. The reason you don't have to remember is that your proof will inevitably rely on a theorem with "x ≠ 0" as one of the premises. (And if that doesn't happen, then the fact that lean defines division strangely isn't relevant to your proof.)
If what you're doing is writing code unaccompanied by proofs, then yes, this is something you'd have to remember.
dnautics · · focus · HN ↗
If you're writing that theorem: Assuming you remember to include it in your premises.
Sometimes the invariant might not be mathematical, it might be social. I recall a story where 1/0 caused a problem because stock issuance uses a 0-share disbursement as a tombstone: to indicate that "this stock account has zeroed out this security and has no remaining ownership". You might not have remembered that and you might have forgotten to record that as a necessary invariant in your proofs. If lean had defined division to have a nonzero denominator, it would have caught the problem even if you didn't know that a zero share disbursement hada a different meaning.
thaumasiotes · · focus · HN ↗
No, you're missing the point. If you're writing that theorem, either (1) you will have to include that premise, and anyone who depends on you will have to satisfy it; or (2) the theorem is true regardless of what happens when you divide by zero, and nobody who depends on you will care. At no point can the division behavior hide something that comes back to bite you.
Mathlib includes theorems of both these types. For an example in a space I've been working with, you can compute the cardinality of a type with Nat.card. This returns a natural number, which is convenient, but since there is no infinitely large natural number, the value of Nat.card for an infinite set is 0.
If you care about the difference, you need ENat.card, which takes different values for empty and infinite types. But you usually won't want to do this, because the value of ENat.card is an extended natural rather than a natural, which makes it a huge pain to work with.
There are several theorems related to Nat.card which take advantage of the dummy "infinite" value of 0 to prove a theorem that is true regardless of what the cardinality might actually be, and omit any premise related to it (which would have taken the form "the type is finite", "the type is uninhabited", or "the type is infinite"). The advantage of doing things that way is that you don't have to detour into the extended naturals, and the validity of your proof is unaffected.
Consider Nat.card_prod, which says that
When α and β are both finite, this says exactly what you'd expect.In the case that α is infinite, Nat.card α will be zero, and therefore the product Nat.card α * Nat.card β will also be zero. It happens that when (α × β) is infinite, Nat.card (α × β) is zero (by definition), so this theorem is correct. The reasoning isn't something you'd want to repeat in those terms in an oral exam, but there are no mistakes, and the stated theorem is true.
> If lean had defined division to have a nonzero denominator
This would be an absolute nightmare.
dnautics · · focus · HN ↗
To write, for a human, yes. An LLM will happily write all the extra discharging statements needed.
However, to review, you have to hold the 1/0 = 0 in mind everywhere and propagate it everywhere, which is difficult for a human. If you had explicit discharging the human can easily remember "oh numbers work the way they ought to"