5 ms·

I think that's an overly formalistic view by the Lean team. When I looked into Lean last (sometime last year), it was a hodgepodge of libraries and constructio

by bmitc 3y ago

I think that's an overly formalistic view by the Lean team. When I looked into Lean last (sometime last year), it was a hodgepodge of libraries and constructions. The maturity of the library depended upon if someone in that area of math had spent a lot of time building one up. There were even competing libraries and approaches. To me, that implies that there's "choice" there, just as there is in mathematics. And a choice could be "buggy". What's to say that the construction of a mathematical structure in Lean is the same as the mathematical structure in "normal" mathematics? So yes, if that statement by the Lean team is accurate, you can build correct things on top of the kernel, but the use of "correct" is a very formal one. It's formally correct in terms of the kernel, but it doesn't mean that it's necessarily mathematically correct. This is to my understanding of course, garnered from trying to get into Lean.

fwip 3y ago
From my understanding, the libraries written in Lean are also formally proven by the kernel. They may be hodge-podge or incomplete, but they are (by construction) not "buggy" in a way that could lead to incorrect proofs, right?
vilhelm_s 3y ago
But like, you can look at what parts of Mathlib this development imports, it's mainly stuff imported by files in this subdirectory https://github.com/leanprover-community/con-nf/tree/main/ConNF/Mathlib https://github.com/leanprover-community/con-nf/tree/main/Con... , and it's pretty basic things: the definition of a permutation, a cardinal number etc. Almost all of these are things that would feature in the first one or two years of an undergraduate math degree (from just quickly scanning it, the most advanced thing I could see is the definition of cofinality of ordinals). It seems practically impossible to me that someone would make a mistake when e.g. defining what a group is, in a way subtle enough to later break this advanced theorem. If you think that people could mess up that, then all of math would be in doubt.
Certhas 3y ago
Your analogy to buggy implementations in ordinary programming languages is deeply flawed though. The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. Bugs at the library level can only appear in the form that formally stated theorems might not be what you think they are. So I object to your characterization that they might be mathematically incorrect. The mathematical content might be different than believed though.
- bmitc 3y ago
  > The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.
  - naasking 3y ago
    > Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further. > (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into. A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.
  - Certhas 3y ago
    Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem. If the runtime is correctly executing the program, then the theorem is proven from the axioms. Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter. So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime. And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.
cvoss 3y ago
I think you are misunderstanding the relationship between the theorem and the proof. You express doubt that the proof is a good one, but then you point to the libraries in Lean as a possible source of incorrectness. The libraries cannot be the source of incorrectness in the proof. They can only be the source of incorrectness in the statement of the theorem. That's why others are challenging you to declare that you don't trust the Lean kernel. A kernel bug is the only thing that can permit incorrectness in the proof. The exact content of the proof doesn't matter for the purposes of deciding whether you should believe the theorem. At all. What matters are two things: 1) Is the theorem correctly stated? That is, does it say what it's supposed to say in the agreed upon (natural or programming) language? 2) Do you trust the Lean kernel (or human reviewer of the proof, if applicable)? If you accept 1) and 2), then you must accept the truth of the theorem. No library used in the construction of the proof, nor any library used in the expression or the proof, can make or break the result. If one uses a library in the statement of the theorem, then that matters. That's letting someone else define some of the terms. And one must investigate whether those definitions are correct in order to decide whether the theorem is stated correctly. If you wish to challenge the work on these grounds, by all means proceed. But you can't say you don't think the proof is a good one for such reasons.

by bmitc 3y ago

fwip 3y ago

From my understanding, the libraries written in Lean are also formally proven by the kernel. They may be hodge-podge or incomplete, but they are (by construction) not "buggy" in a way that could lead to incorrect proofs, right?

vilhelm_s 3y ago

But like, you can look at what parts of Mathlib this development imports, it's mainly stuff imported by files in this subdirectory https://github.com/leanprover-community/con-nf/tree/main/ConNF/Mathlib https://github.com/leanprover-community/con-nf/tree/main/Con... , and it's pretty basic things: the definition of a permutation, a cardinal number etc. Almost all of these are things that would feature in the first one or two years of an undergraduate math degree (from just quickly scanning it, the most advanced thing I could see is the definition of cofinality of ordinals). It seems practically impossible to me that someone would make a mistake when e.g. defining what a group is, in a way subtle enough to later break this advanced theorem. If you think that people could mess up that, then all of math would be in doubt.

Certhas 3y ago

Your analogy to buggy implementations in ordinary programming languages is deeply flawed though. The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. Bugs at the library level can only appear in the form that formally stated theorems might not be what you think they are. So I object to your characterization that they might be mathematically incorrect. The mathematical content might be different than believed though.

bmitc 3y ago
> The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.
- naasking 3y ago
  > Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further. > (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into. A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.
- Certhas 3y ago
  Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem. If the runtime is correctly executing the program, then the theorem is proven from the axioms. Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter. So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime. And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.

cvoss 3y ago

I think you are misunderstanding the relationship between the theorem and the proof. You express doubt that the proof is a good one, but then you point to the libraries in Lean as a possible source of incorrectness. The libraries cannot be the source of incorrectness in the proof. They can only be the source of incorrectness in the statement of the theorem. That's why others are challenging you to declare that you don't trust the Lean kernel. A kernel bug is the only thing that can permit incorrectness in the proof. The exact content of the proof doesn't matter for the purposes of deciding whether you should believe the theorem. At all. What matters are two things: 1) Is the theorem correctly stated? That is, does it say what it's supposed to say in the agreed upon (natural or programming) language? 2) Do you trust the Lean kernel (or human reviewer of the proof, if applicable)? If you accept 1) and 2), then you must accept the truth of the theorem. No library used in the construction of the proof, nor any library used in the expression or the proof, can make or break the result. If one uses a library in the statement of the theorem, then that matters. That's letting someone else define some of the terms. And one must investigate whether those definitions are correct in order to decide whether the theorem is stated correctly. If you wish to challenge the work on these grounds, by all means proceed. But you can't say you don't think the proof is a good one for such reasons.