4 ms·

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

by 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.
- svat 3y ago
  My reading is that for an individual theorem or proof, having it checked by computer may well be more "secure". But a culture where all mathematics is done (only) by computer would be worse, because you'd have outsourced the thinking and quest for understanding which was the point in the first place.
  - Tainnor 3y ago
    The way theorem provers work right now, it's still a human that has to come up with the proof, the theorem prover just verifies it. But yes, I wouldn't want computer proofs to "replace" the proofs we have now.
deleted 3y ago
[deleted]

by svat 3y ago

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.

svat 3y ago
My reading is that for an individual theorem or proof, having it checked by computer may well be more "secure". But a culture where all mathematics is done (only) by computer would be worse, because you'd have outsourced the thinking and quest for understanding which was the point in the first place.
- Tainnor 3y ago
  The way theorem provers work right now, it's still a human that has to come up with the proof, the theorem prover just verifies it. But yes, I wouldn't want computer proofs to "replace" the proofs we have now.

deleted 3y ago

[deleted]