Formal Proof—The Four- Color Theorem

1 Formal Proof The Four- Color TheoremGeorges GonthierThe Tale of a BrainteaserFrancis Guthrie certainly did it, when he coined hisinnocent little coloring puzzle in 1852. He man-aged to embarrass successively his mathematicianbrother, his brother s professor, Augustus de Mor-gan, and all of de Morgan s visitors, who couldn tsolve it; the Royal Society, who only realized tenyears later that Alfred Kempe s 1879 solution waswrong; and the three following generations ofmathematicians who couldn t fix it [19].Even Appel and Haken s 1976 triumph [2] had ahint of defeat: they d had a computer do the prooffor them! Perhaps the mathematical controversyaround the proof died down with their book [3]and with the elegant 1995 revision [13] by Robert-son, Saunders, Seymour, and Thomas. Howeversomething was still amiss: both proofs combineda textual argument, which could reasonably bechecked by inspection, with computer code thatcould not.

2 Worse, the empirical evidence providedby running code several times with thesameinputis weak, as it is blind to the most common causeof computer error: programmer some thirty years, computer science hasbeen working out a solution to this problem: for-mal program proofs. The idea is to write code thatdescribes not onlywhatthe machine should do,but alsowhyit should be doing it a Formal proofof correctness. The validity of the proof is anobjective mathematical fact that can be checkedby adifferentprogram, whose own validity canbe ascertained empirically because it does runonmanyinputs. The main technical difficulty isthat Formal proofs are very difficult to produce,Georges Gonthier is a senior researcher at MicrosoftResearch Cambridge. His email address with a language rich enough to express 2000 we tried to produce such a proof forpart of code from [13], just to evaluate how thefield had progressed.

3 We succeeded, but now anew question emerged: was the statement of thecorrectness proof (thespecification) itself correct?The only solution to that conundrum was to for-malize theentireproof of the Four- Color Theorem ,not just its code. This we finally achieved in we tackled this project mainly to ex-plore the capabilities of a modern Formal proofsystem at first, to benchmark speed we werepleasantly surprised to uncover new and ratherelegant nuggets of mathematics in the process. Inhindsight this might have been expected: to pro-duce a Formal proof one must make explicit everysingle logical step of a proof; this both providesnew insight in the structure of the proof, andforces one to use this insight to discover everypossible symmetry, simplification, and general-ization, if only to cope with the sheer amount ofimposed detail. This is actually how all of sections Combinatorial Hypermaps (p. 1385) and TheFormal Theorem (p.)

4 1388) came about. Perhapsthis is the most promising aspect of Formal proof:it is not merely a method to make absolutely surewe have not made a mistake in a proof, but also atool that shows us and compels us to understandwhy a proof this article, the next two sections containbackground material, describingthe original proofand the Coq Formal system we used. The followingtwo sections describe the sometimes new math-ematics involved in the formalization. Then thenext two sections go into some detail into the twomain parts of the Formal proof: reducibility and1382 Notices of the AMSV olume55, Number11unavoidability; more can be found in [8]. The Coqcode (available at the same address) is the ultimatereference for the intrepid, who should bone up onCoq [4, 16, 9] Puzzle and Its SolutionPart of the appeal of the four Color problem is thatits statementTheorem regions of any simple planar mapcan be colored with only four colors, in such a waythat any two adjacent regions have different on the one hand be understood even byschoolchildren as four colors suffice to Color anyflat map and on the other hand be given a faith-ful, precisemathematicalinterpretationusing onlybasic notions in topology, as we shall see in thesection The Formal Theorem .

5 The first step in the proof of the Four- ColorTheorem consists precisely in getting rid of thetopology, reducing an infinite problem in analysisto a finite problem in combinatorics. This is usual-ly done by constructing the dual graph of the map,and then appealing to the compactness theoremof propositional logic. However, as we shall seebelow, the graph construction is neither neces-sary nor sufficient to fully reduce the problem , we ll simply restrict the rest of thisoutline to connected finite maps whose regionsare finite polygons and which arebridgeless: everyedge belongs to exactly two polygons. Every suchpolyhedralmap satisfies the Euler formulaN E+F=2whereN,E, andFare respectively the number ofvertices (nodes), sides (edges), and regions (faces)in the next step consists in further reducing tocubicmaps, where each node is incident to exactlythree edges, by covering each node with a a cubic map we have 3N=2E, which com-bined with the Euler formula gives us that theaverage number of sides (orarity) of a face is2E/F=6 12 proof proceeds by induction on the size ofthe map; it is best explained as a refinement ofKempe s flawed 1879 proof [12].

6 Since its averagearity is slightly less than 6, any cubic polyhedralmap must contain ann-gon withn <6, , one ofthe following map suchconfigurationconsists of a completekernelface surrounded by aringof partial an edge of a digon or triangle yields asmaller map, which is Four- colorable by coloring uses at most three colors for thering, leaving us a free Color for the kernel face,so the original map is also Four- colorable. Erasingan appropriate pair of opposite edges disposes ofthe square configuration the pentagon case, however, it is necessaryto modify the inductive coloring to free a ringcolor for the kernel face. Kempe tried to do this bylocally inverting the colors inside atwo-toned max-imal contiguous group of faces (a Kempe chain ).By planarity, chains cannot cross, and Kempeenumerated their arrangements and showed thatconsecutive inversions freed a ring Color . Alas, it isnot always possible to do consecutive inversions,as inverting one chain can scramble other took ten years to spot this error and almost acentury to fix correct proof gives up on pentagons andturns to largerreducibleconfigurations for whichKempe s argument is sound.

7 The first such config-uration, which has ring-size 6, was discovered byBirkhoff in 1913 [5]:Birkhoff also showed that all configurations withring-size less than 6 are reducibleexceptthepentagon; thus any minimal counter-example tothe Theorem must beinternally 6-connected(we llrefer to this as the Birkhoff lemma ).As we ll see below, showing that a given config-uration is reducible is fairly straightforward, butvery laborious: the number of cases to considerincreases geometrically to about 20,000,000 forring-size 14, and 137 of the 633 configurationsused in the proof [13] are of that final part of the proof shows that reducibleconfigurations areunavoidable,using arefinementof the average-arityargumentpublished by Heeschin 1969 [11]. The idea is to look for reducible con-figurations near faces whose arity averaged overtheir 2-neighborhood is less than 6; the averag-ing is done by transfering (discharging) fractionsof arities between adjacent faces according to asmall set of local patterns: the discharged arityof a faceais (a)= (a)+Pb(Tba Tab)December2008 Notices of the AMS1383where (a)is the original arity ofa, andTbais thearity fraction transfered fromb.

8 Thus the averagedischarged arity remains 6 12/F < whose discharged arity is lessthan 6. This enumeration is fairly complex, butnot as computationally intensive as the reducibil-ity checks: the search is heavily constrainedas the neighborhoods consist of two disjointconcentric rings of 5+-gons. Indeed in [13] re-ducible configurations are always found inside the2-neighborhoods, and the central face is a 7+ and the Calculus of InductiveConstructionsThe Coq Formal proof system (orassistant) [4,16], which we used for our work is based ona version of higher-order logic, the Calculus ofinductive Constructions (CiC) [6] whose specificfeatures propositions as types, dependent types,and reflection all played an important part in thesuccess of our have good reason to leave the familiar,dead-simple world of untyped first-order logic forthe more exotic territory of Type Theory [10, 4]. Infirst-order logic, higher-level ( meta ) argumentsare second-class citizens: they are interpreted asinformal procedures that should be expandedout to primitive inferences to achieve full is fine in a non- Formal proof, but rapidlybecomes impractical in a Formal one because oframping complexity.

9 Computer automation canmitigate this, but type theory supplies a muchmore satisfactory solution, levelling the playingfield by providing a language that can can indeed be observed even with thesimplest first-order type system. Consider thecommutativity of integer addition, x, y N, x+y=y+xThere are two hidden premises,x Nandy N,that need to be verified separately every time thelaw is used. This seems innocuous enough, exceptxandymay be replaced by huge expressions forwhich thex, y Npremises are not obvious, evenfor machine automation. By contrast, the typedversion of commutativity x, y: Nat, x+y=y+xcan be applied to any expressionA+Bwithoutfurther checks, because the premises follow fromthe wayAandBare written. We are simply notallowed to write drivel such as 1+true, and conse-quently we don t need to worry about its existence,even in a fully Formal proof we have proof bynotation .Our Formal proof uses this, and much more:proof types, dependent types, and reflection, aswe will now types are types that encode logic (they realso called propositions-as-types ).

10 The encod-ing exploits a strong similarity between type andlogic rules, which is most apparent when bothare written in natural deduction style (see [10] inthis issue), , consider function application andmodus ponens (MP):f:A B x:Af x:BA B ABThe rules are identical if one ignores the terms tothe left of : . However these terms can also beincluded in the correspondence, by interpretingx:Aand xprovesA rather than xis of typeA .In the above we have thatf xprovesBbecausexprovesAandfprovesA B, so the applica-tionf xon the left denotes the MP deduction onthe right. This holds in general: proof types areinhabited by proof is entirely based on this correspondence,which goes back to Curry and Howard. CiC is aformalism without a Formal logic, a sensible sim-plification: as we ve argued we need types anyway,so why add a redundant logic? The availabilityof proof objects has consequences both for ro-bustness, as they provide a practical means ofstoring and thus independently checking proofs,and for expressiveness, as they let us describeand prove algorithms that create and processproofs correspondence in CiC is not limited toHerbrand term and minimal logic; it interpretsmost data and programming constructs commonin computer science as useful logical connectivesand deduction rules, , pairs as and x:A y:Bhx, yi:A Bu:A :A :BA BA BA BA Btagged unions as or , conditional (if-then-else)as proof by cases, recursive definitions as proofby induction, and so on.