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.
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.
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.
Do you have a reference for the ‘discover that the previous version was incomplete’ part?
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.