Formal Proof—The Four- Color Theorem

By Georges Gonthier. 2008

561 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/1921899c005c4cf1ee15358377c2f63eb6c99d07

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

A Machine-Checked Proof of the Odd Order Theorem (2013, methodology): “For example, Appel and Haken’s proof of the four-color theorem [1] has been verified [16] in the Coq system [7], and Thomas Hales’ Flyspeck project [23] is working towards verifying a proof of the Kepler conjecture, which Hales himself first established with contributions by Samuel Ferguson.”
Intuitionistic Type Theory (2016, background): “This point has been emphasized by Gonthier (2008) in the paper in which he describes his proof of the Four Colour Theorem: The approach that proved successful for this proof was to turn almost every mathematical concept into a data structure or a program in the Coq system, thereby converting the…”
Learning to Reason in Large Theories without Imitation (2019, background): “uman proofs, and the considerations that informed our ﬁnal design. Much of mathematics that has been formalized by humans is in pursuit of formalizing certain theorems such as the four color theorem [Gonthier, 2008] and the Kepler conjecture [Hales et al., 2017]. Since formalization is a challenging”
The simplicial model of Univalent Foundations (after Voevodsky) (2012, unknown): “…on the Calculus of Inductive Constructions (a closely related dependent type theory), which has shown itself feasible for large-scale formal veriﬁcation of mathematics, with developments including formal proofs of the Four-Colour Theorem [Gon08] and the Feit-Thompson (Odd Order) Theorem [GAA + 13].”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, background): “Hence, projects such as the formalisation of complicated mathematical results [Gonthier et al., 2008, Avigad et al., 2007, Gonthier et al., 2013, Scholze, 2021] and operating system kernel veriﬁcation [Klein et al., 2009] are done in interactive theorem provers, often based on higher-order logic or…”
Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017, background): “…et al., 2009; Chli-pala, 2013; Chen et al., 2015), which has aimed to prove properties of computer programs, and formal mathematics (Rudnicki, 1992; Gonthier, 2008; Gonthier et al., 2013; Hales et al., 2015), which has aimed to formally represent and generate machine-checkable proofs of…”
History of Interactive Theorem Proving (2014, background): “The first notable exception to this state of affairs was arguably Gonthier’s machine-checked proof [Gonthier, 2005; Gonthier, 2008] of the 4-color theorem, originally proved in 1976 [Appel and Haken, 1976].”