Blueberry comments on What Cost for Irrationality? - Less Wrong

59 Post author: Kaj_Sotala 01 July 2010 06:25PM

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

Comments (113)

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

Comment author: Douglas_Knight 04 July 2010 06:37:37AM 3 points [-]

Actually, Georges Gonthier did give a formal (computer-verified) proof of the four-color theorem. Also, I believe that before that, every 5 years, someone would give a simpler version of the original proof and discover that the previous version was incomplete.

Comment author: Blueberry 04 July 2010 06:51:04AM 0 points [-]

Wow, thanks! I didn't realize that. It looks like Gonthier's proof was verified with Coq, so it's still not clear that it should count as a proof. I'm still waiting for the Book proof.