= 27d567bc2d48d9f40e9ccc20ea370b15)
DanielLC 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.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
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.
Learning to use automated proof checkers might be a valuable rationalist-training technique.
Struggling with a compiler or a proof checker (They're very similar by the Curry-Howard isomorphism) is an interesting (and perhaps depressing) learning experience. The computer reveals how many "details" you can overlook, and how frequently your gut or instinct is just wrong. Often the "details" are the vast majority of the final result.
Some of the appeal that LessWrong has for programmers might be explained by their exposure to this sort of learning experience.
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.