Khoth comments on Making Reasoning Obviously Locally Correct - Less Wrong

19 Post author: JGWeissman 12 March 2011 07:41PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (23)

You are viewing a single comment's thread. Show more comments above.

Comment author: DanielLC 12 March 2011 08:14:15PM 3 points [-]

From what I understand, being completely explicit in math is quite rare. I figure it doesn't really count until you can run it through an automated proof checker.

Comment author: Khoth 12 March 2011 09:46:09PM 7 points [-]

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.

Comment author: djcb 13 March 2011 12:05:15PM 0 points [-]

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.