In 2005, we achieved the formalization of the entire proof of the Four-Color Theorem, not just its code. While we tackled this project mainly to explore the capabilities of a modern formal proof system —at first, to benchmark speed— we were pleasantly surprised to uncover new and rather elegant nuggets of mathematics in the process. In hindsight this might have been expected: to produce a formal proof one must make explicit every single logical step of a proof; Perhaps this is the most promising aspect of formal proof: it is not merely a method to make absolutely sure we have not made a mistake in a proof, but also a tool that shows us and compels us to understand why a proof works.
In this article, the next two sections contain background material, describing the original proof and the Coq formal system we used. The following two sections describe the sometimes new mathematics involved in the formalization. Then the next two sections go into some detail into the two main parts of the formal proof: reducibility and unavoidability. The Coq code (available at the same address) is the ultimate reference for the intrepid, who should bone up on Coq beforehand.
Lire maintenant ?