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.
This. Lean does not remove human responsibility, but it does assist in reducing the surface that the human needs to inspect and verify.
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.
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!
What people are telling you is you need to check the signature of negative_one_has_a_real_square_root (which includes the definition of Real). Generally this is an easy task. Did you define things the way that you meant to define them to make the statement that you meant to make? Then you can trust that the 500k lines that prove it are fine.
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
Right but... the difference between "a robot may not injure a human being" and "a robot must injure a human being" is quite important in the real world, even if the "mathematical content is correct". And if my silly example is too contrived, it still seems like this sort of thing happens all the time:
That paper seems to just be saying that people's benchmarks are bad. Like, yeah, obviously don't consider the problem solved if the bot used sorry or axiom. This is trivial to check for and consider a compile error. It's (literally) the same as just not allowing throwing exceptions in a program. And vacuous statements aren't actually a problem. And they claim that sometimes it makes mistakes formalizing an informal statement, but that this becomes noticeable when you try to actually prove it. This is like if it forgot a parameter when it was defining a function prototype. When it actually goes to write the function, it realizes it needed some extra information, so it'll just add it. So, again, what's the problem? This isn't the type of error that can go uncaught because it won't be able to proceed with the actual proof unless it's actually true, in which case, great, it proved a stronger statement than was asked for.
A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.
You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.
After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.
I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.
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)
> Surely “the proof is the one you think it is” is the whole ballgame?
No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> 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.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.
The core of a proof checker is a formally validated core that is based on a small amount of concepts. Every single line in the proof reduces to that core, therefore, as long as you can trust the core, you can trust the execution of the proofs.
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
Yes but why do we write the last bit as an aside as if that’s not a massive yawning black hole for errors to hide in? All the other stuff is irrelevant, just like when Haskell and Rust people claim that if their code compiles it is correct.
Because in practice, it's very straightforward to check that all of the types for class members are what you expect. Especially when you actually use that class in other code. You have things in mind that the class should do. If you get compile errors doing those things, you notice the inconsistency.
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.
You only need to trust your spec and the Lean kernel. If you trust those two things, you don't ever need to manually inspect or check the proof. That's the job of the Lean kernel, and your trust of it transfers over to trust of any proof verified by it.
Making sure your spec is correct -- and that it's expressed at a level of abstraction that both captures what matters, without overly constraining implementation details within the repo -- is the hard part. The more the spec constrains implementation details, the less you can ask an agent to, e.g., try many ideas to optimize a specific component without breaking correctness. And of course if the spec isn't enforcing what you wanted it to, then all the proofs don't count for much.
Some people say the spec issues are enough reason to avoid formal methods, but I'm not convinced. Part of me truly thinks AI formal methods is the future of a lot of software engineering. The basis of that belief for me is that the industry has collectively put almost no effort yet into solving the spec problem, and that's because for decades formal methods were too expensive to seriously consider most of the time. Now that AI is fundamentally shifting the economics, there's now, for the first time ever, a real incentive to try to solve the spec problem. And frankly it seems solvable to me; I view it as more of a product design and UI problem than a purely technical one.
Well, the statement can be the 500k line part if it's generated with an LLM. But I think some people miss the point of Lean when they use LLM like that.
> 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.
1/0 is 0 in lean, though it may not be a problem.
<a href="https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/" rel="nofollow">https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
So, you think it's important for other people to learn Lean's model of type theory before using it to do entirely unrelated proofs, but you see no reason you should know anything about how basic arithmetic works?
> 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"
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 ↗
6gvONxR4sf7o · · focus · HN ↗
ubj · · focus · HN ↗
Now, there is also debate about what is lost when humans don't understand the proof body itself. It's a fair concern, and one we'll probably be wrestling with for some years.
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 ↗
ndriscoll · · focus · HN ↗
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
thom · · focus · HN ↗
<a href="https://proceedings.mlr.press/v306/ammanamanchi26a.html" rel="nofollow">https://proceedings.mlr.press/v306/ammanamanchi26a.html
ndriscoll · · focus · HN ↗
A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.
You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.
After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.
I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.
thom · · focus · HN ↗
rramadass · · focus · HN ↗
Validating a Lean Proof - <a href="https://lean-lang.org/doc/reference/latest/ValidatingProofs/" rel="nofollow">https://lean-lang.org/doc/reference/latest/ValidatingProofs/
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
SkiFire13 · · focus · HN ↗
No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> 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.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.
whateverboat · · focus · HN ↗
Therefore, whether the proof is generated by LLM or not is immaterial, since you know that core will always evaluate correctly whether the proof is correct or not.
What is much more important is to evaluate the theorem and determine if that theorem is actually the theorem you wanted to prove.
thom · · focus · HN ↗
ndriscoll · · 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.
nilkn · · focus · HN ↗
Making sure your spec is correct -- and that it's expressed at a level of abstraction that both captures what matters, without overly constraining implementation details within the repo -- is the hard part. The more the spec constrains implementation details, the less you can ask an agent to, e.g., try many ideas to optimize a specific component without breaking correctness. And of course if the spec isn't enforcing what you wanted it to, then all the proofs don't count for much.
Some people say the spec issues are enough reason to avoid formal methods, but I'm not convinced. Part of me truly thinks AI formal methods is the future of a lot of software engineering. The basis of that belief for me is that the industry has collectively put almost no effort yet into solving the spec problem, and that's because for decades formal methods were too expensive to seriously consider most of the time. Now that AI is fundamentally shifting the economics, there's now, for the first time ever, a real incentive to try to solve the spec problem. And frankly it seems solvable to me; I view it as more of a product design and UI problem than a purely technical one.
rzmmm · · 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 ↗
fooker · · focus · HN ↗
howling · · focus · HN ↗
1/0 is 0 in lean, though it may not be a problem. <a href="https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/" rel="nofollow">https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
thaumasiotes · · 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"
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."
whateverboat · · focus · HN ↗