Agreed. In fact, I suspect that unless you actually can run it through an automatic proof checker, humans are more likely to spot an error in the vague proof. People aren’t terribly good at reading pages of verbose symbol manipulation without glazing over.
Indeed. Case in point Principia Mathematica as discussed in the Stephen Wolfram’s blog, with the amusing note about the proof for the proposition that 1 + 1 = 2.
Agreed. In fact, I suspect that unless you actually can run it through an automatic proof checker, humans are more likely to spot an error in the vague proof. People aren’t terribly good at reading pages of verbose symbol manipulation without glazing over.
Indeed. Case in point Principia Mathematica as discussed in the Stephen Wolfram’s blog, with the amusing note about the proof for the proposition that 1 + 1 = 2.