6 ms·
It also sounds like a motivating example for machine-checked proofs: if one could feed Mochizuki's proof into Coq or something and be assured that it was correc
by 336f5 11y ago
It also sounds like a motivating example for machine-checked proofs: if one could feed Mochizuki's proof into Coq or something and be assured that it was correct, even if only in a purely formal sense, I suspect there would be much more interest in grappling with the concepts to understand what the proof is doing, whether it's acceptable, and why the proof is correct. As it stands, there's the risk of a wild goose chase.
- jordigh 11y agoIf Mochizuki were able to write a machine-checkable proof, he would also be able to write a human-checkable proof, which is far easier to write.
- kinghajj 11y agoWell, supposedly he did write a human-checkable proof--it's just that the reviewer must be familiar with several of his novel ideas. Like any human-intended proof, there's an assumption of foreknowledge.