Ver el código de «Formal Proof: The Four-Color Theorem»

G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf ''Formal Proof: The Four-Color Theorem'']. Notices of the AMS, Vol. 55, N. 11 (2008) p.1382-1393.
----
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 ﬁrst, 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, simpliﬁcation, 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.''

[[User:Jalonso|José A. Alonso]] 11 Diciembre 2008
[[Category:Lecturas]]