3 ms·

I find his scepticism about proof assistants like Lean a bit weird. Of course, there is never absolute certainty, but there are degrees. A proof in Lean is a qu

I find his scepticism about proof assistants like Lean a bit weird. Of course, there is never absolute certainty, but there are degrees. A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong, which is possible but less likely than a flaw in a proof that hasn't seen much scrutiny because it's rather unimportant (of course, "big" results get so much scrutiny that it's also very unlikely that they were wrong).

davidgrenier 3y ago
I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.
- Tainnor 3y ago
  Yeah it's likely he hasn't worked much with Lean and may have some misconceptions around it.
- SkiFire13 3y ago
  The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.
- robinzfc 3y ago
  Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434 https://mathoverflow.net/a/291351/163434) to a MathOverflow question.
  - calf 3y ago
    It would be interesting to see some computer-aided proof expert write a possible counter-response to the article.
svat 3y ago
I wouldn't characterize him as being sceptical about Lean; this is what he says: > Some terrific developments have happened with proof verification. Like [the proof assistant] Lean, which has allowed mathematicians to verify many proofs, while also helping the authors better understand their own work, because they have to break down some of their ideas into simpler steps to feed into Lean for verification. […] I’m not saying that I believe something like Lean is going to make a lot of errors. […] They can be a very valuable tool for getting things right — particularly for verifying mathematics that rests heavily on new definitions that are not easy to analyze at first sight. There’s no debate that it’s helpful to have new perspectives, new tools and new technology in our armory. In between (the "[…]"s above), he says: > But is this foolproof? Is a proof a proof just because Lean agrees it’s one? In some ways, it’s as good as the people who convert the proof into inputs for Lean. Which sounds very much like how we do traditional mathematics. […] I’m just not sure it’s any more secure than most things done by humans. […] I’m afraid I have a lot of skepticism about the role of computers. […] what I shy away from is the concept that we’re now going to have perfect logical machines that produce correct theorems. You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on. The latter part is less about the correctness and more about community: the main goal of mathematics is not merely a "true" theorems, but (human) mathematical understanding. I wrote an answer about this on math.SE in 2014 (mostly quoting Thurston and Rota): https://math.stackexchange.com/questions/632705/why-are-mathematical-proofs-that-rely-on-computers-controversial/632745#632745 https://math.stackexchange.com/questions/632705/why-are-math...
- epgui 3y ago
  I agree very much with you... but it seems to me like theorem provers / computers can be a really helpful tool in building trust and understanding between people or between groups of people, in ways that printed paper can't quite match.
- Tainnor 3y ago
  I agree that a big part of proving thing is understanding intuitively "why" they are true. That's part of the reasons why I don't think we'll just write proofs in Lean in 50 years and leave it at that (the other reason is that, at least for now, those systems are very "stupid" and need a lot of handholding to prove facts that any maths undergraduate would understand to be true). But when he says that he doesn't believe that a proof in Lean is "more secure than most things done by humans" I fundamentally disagree.
epgui 3y ago
> A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong That, or an error in the specification (ie.: not the implementation). (I very much am with you that his attitude / way of framing it is a bit weird)
- Jweb_Guru 3y ago
  I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's kernel, it will almost never invalidate a Lean proof, because bugs in the Lean kernel (or the kernels of other proof assistants) are, just like with normal programs, almost always bugs dealing with edge cases testing the boundaries of mathematics or syntax, not things that show up in everyday proofs. Coq has fixed numerous proofs of False and, to my knowledge, these fixes have never ended up invalidating a "real" proof that wasn't specifically designed to test these kinds of edge cases. Proofs are far more often broken by changes to the surface syntax (e.g. inference algorithms or the tactic language) than by changes to the kernel. Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics. (I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).
  - reuben364 3y ago
    Your "adverserial" mathematician phrasing made me chuckle at the the thought of a future where you have cybersec jobs in automated journals to prevent shady academics from using kernel bugs to spam fake submissions.
jeremyjh 3y ago
I read it more as him saying that at the end of the day a human is inputting symbols into Lean, and a human is interpreting the meaning of the proof that Lean has verified. Not that the mechanics of the proof checking are in doubt, but that that meaning of it all is still a social consensus.

davidgrenier 3y ago

I think his argument was restricted to a human-produced mathematical result being ported to a Lean program where one would be just as likely to commit a mistake. However I disagree as well, I recall the difficulty of expressing what I wanted to Coq being a barrier to expressing it incorrectly.

Tainnor 3y ago
Yeah it's likely he hasn't worked much with Lean and may have some misconceptions around it.
SkiFire13 3y ago
The thing about proof checkers is that they won't accept invalid proofs (assuming their internal axioms are consistents...), so if you make a mistake there it will simply reject your proof. The only place where it won't catch some mistakes is in proposition you want to prove, because the only way for it to know what you want to prove if for you to tell it, but that's much easier to humanly verify.
robinzfc 3y ago
Having worked with a proof assistant is what separates you from Granville (the interviewee in the article). If he had formalized at least a couple of proofs he would not have written things like "people who convert the proof into inputs for Lean". One does not "convert the proof into inputs for Lean" for a simple reason that a proof written in a formal proof language usually contains much more information than the informal prototype. At best one can try to express similar ideas, but it is far from converting a proof from one form to another. If he had formalized a couple of hundred he would have gained a different opinion on the quality of informal proofs as well. A nice list of typical mistakes can be found in this [answer](https://mathoverflow.net/a/291351/163434 https://mathoverflow.net/a/291351/163434) to a MathOverflow question.
- calf 3y ago
  It would be interesting to see some computer-aided proof expert write a possible counter-response to the article.

svat 3y ago

I wouldn't characterize him as being sceptical about Lean; this is what he says: > Some terrific developments have happened with proof verification. Like [the proof assistant] Lean, which has allowed mathematicians to verify many proofs, while also helping the authors better understand their own work, because they have to break down some of their ideas into simpler steps to feed into Lean for verification. […] I’m not saying that I believe something like Lean is going to make a lot of errors. […] They can be a very valuable tool for getting things right — particularly for verifying mathematics that rests heavily on new definitions that are not easy to analyze at first sight. There’s no debate that it’s helpful to have new perspectives, new tools and new technology in our armory. In between (the "[…]"s above), he says: > But is this foolproof? Is a proof a proof just because Lean agrees it’s one? In some ways, it’s as good as the people who convert the proof into inputs for Lean. Which sounds very much like how we do traditional mathematics. […] I’m just not sure it’s any more secure than most things done by humans. […] I’m afraid I have a lot of skepticism about the role of computers. […] what I shy away from is the concept that we’re now going to have perfect logical machines that produce correct theorems. You have to acknowledge that we can’t be sure things are correct with computers. Our future has to rely on the sense of community that we have relied on throughout the history of science: that we bounce things off one another. That we talk to people who look at the same thing from a completely different perspective. And so on. The latter part is less about the correctness and more about community: the main goal of mathematics is not merely a "true" theorems, but (human) mathematical understanding. I wrote an answer about this on math.SE in 2014 (mostly quoting Thurston and Rota): https://math.stackexchange.com/questions/632705/why-are-mathematical-proofs-that-rely-on-computers-controversial/632745#632745 https://math.stackexchange.com/questions/632705/why-are-math...

epgui 3y ago
I agree very much with you... but it seems to me like theorem provers / computers can be a really helpful tool in building trust and understanding between people or between groups of people, in ways that printed paper can't quite match.
Tainnor 3y ago
I agree that a big part of proving thing is understanding intuitively "why" they are true. That's part of the reasons why I don't think we'll just write proofs in Lean in 50 years and leave it at that (the other reason is that, at least for now, those systems are very "stupid" and need a lot of handholding to prove facts that any maths undergraduate would understand to be true). But when he says that he doesn't believe that a proof in Lean is "more secure than most things done by humans" I fundamentally disagree.

epgui 3y ago

> A proof in Lean is a quite strong guarantee, you'd basically have to have a bug in Lean's core for it to be wrong That, or an error in the specification (ie.: not the implementation). (I very much am with you that his attitude / way of framing it is a bit weird)

Jweb_Guru 3y ago
I will go further (since there are certainly bugs in the kernels of proof assistants, more frequently than you might imagine). Even if there is a bug in Lean's kernel, it will almost never invalidate a Lean proof, because bugs in the Lean kernel (or the kernels of other proof assistants) are, just like with normal programs, almost always bugs dealing with edge cases testing the boundaries of mathematics or syntax, not things that show up in everyday proofs. Coq has fixed numerous proofs of False and, to my knowledge, these fixes have never ended up invalidating a "real" proof that wasn't specifically designed to test these kinds of edge cases. Proofs are far more often broken by changes to the surface syntax (e.g. inference algorithms or the tactic language) than by changes to the kernel. Obviously, this is not foolproof against malicious "adversarial" mathematicians, so knowing something was proved in Lean still requires some degree of checking. But it does make it pretty extraordinarily unlikely that a false proof in a proof assistant was arrived at by accident, which is far from the case with the "old" way of doing mathematics. (I'd also add that the concern about getting the specification of a design wrong is something that rarely lasts longer than attempts to actually use it to prove anything nontrivial, since the proofs won't go through, but there at least can be a lot of debate about how to interpret specifications in some fields [e.g. computer science] or whether certain specs are "actually" equivalent to the statements someone wants to prove, especially for stuff like category theory where manual proofs have a good deal of handwaving... but these are minor technical issues compared to the viewpoint of the article).
- reuben364 3y ago
  Your "adverserial" mathematician phrasing made me chuckle at the the thought of a future where you have cybersec jobs in automated journals to prevent shady academics from using kernel bugs to spam fake submissions.

jeremyjh 3y ago

I read it more as him saying that at the end of the day a human is inputting symbols into Lean, and a human is interpreting the meaning of the proof that Lean has verified. Not that the mechanics of the proof checking are in doubt, but that that meaning of it all is still a social consensus.