Formal Proof: The Four-Color Theorem

G. Gonthier Formal Proof: The Four-Color Theorem. Notices of the AMS, Vol. 55, N. 11 (2008) p.1382-1393.

---

Este trabajo es el segundo artículo del número de Diciembre de 2008 de las Notices of the AMS dedicado a las demostraciones formales. El artículo describe la formalización que hizo el autor en Coq del teorema de los cuatros colores. Además, contiene algunos comentarios generales sobre la formalización del razonamiento. Por ejemplo, sobre la motivación inicial del proyecto y los resultados no previstos:

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; this both provides new insight in the structure of the proof, and forces one to use this insight to discover every possible symmetry, simplification, and generalization, if only to cope with the sheer amount of imposed detail. This is actually how all of sections

y la mejora de las razones del funcionamiento de las demostraciones:

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.

José A. Alonso 11 Diciembre 2008