> It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with. Only because we're n

> It's like saying that a non-machine-checkable mathematical proof is not a proof - something few working mathematicians would agree with. Only because we're not ready for that yet. Given the current technology (Coq, Agda, Mizar etc.), writing a machine-checkable proof is unbelievably tedious. That doesn't mean it wouldn't be welcome; many published papers, even widely accepted ones, have later been found to contain errors. [1] [2] [1] https://mathoverflow.net/questions/35468/widely-accepted-mathematical-results-that-were-later-shown-to-be-wrong https://mathoverflow.net/questions/35468/widely-accepted-mat... [2] https://lamport.azurewebsites.net/tla/proof-statistics.html https://lamport.azurewebsites.net/tla/proof-statistics.html