3 ms·
Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as l
by nynox 6y ago
Following this proof tree idea, this recent paper https://arxiv.org/abs/2102.03044 https://arxiv.org/abs/2102.03044 suggests to think of proofs of theorems as large trees, a tiny subset of which needs to be made explicit to convey the confidence the rest could be written out (if ever needed).
- carapace 6y agoDoes that presuppose that it's computationally expensive to verify proofs? If so, isn't that kind of unrealistic?
- nynox 6y agoVerifying fully formalized proofs is cheap. What is expensive is to produce such formalized proofs. More precisely, to formalize a proof written in a typical math paper is extremely time-consuming and not so informative (that's why it's almost never done in practice).
- carapace 6y agoAh, cheers. :) But doesn't that bring us full-circle to Buzzard's point? Isn't that why he's saying, "Hey gang, let's do math with machines." in the first place?