Khoth comments on Making Reasoning Obviously Locally Correct - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (23)
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.
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.