3 ms·
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
by 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 agoMy 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 agoThe 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.