A pictorial proof of the Four Colour Theorem
Abstract
We give a pictorial, and absurdly simple, proof that transparently illustrates why four colours suffice to chromatically differentiate any set of contiguous, simply connected and bounded, planar spaces; by showing that there is no minimal planar map. We show, moreover, why the proof cannot be expressed within classical graph theory.
keywords:
contiguous area, four colour theorem, planar map, simply connected.2010 Mathematics Subject Classification. 05C15
DECLARATIONS Funding: Not applicable Conflicts of interest/Competing interests: Not applicable Availability of data and material: Not applicable Code availability: Not applicable Authors’ contributions: Not applicable
1 Introduction
Although the Four Colour Theorem 4CT is considered passé (see §1.1), we give a pictorial, and absurdly simple, proof222Extracted from [An21], §1.G: Evidence-based (pictorial), pre-formal, proofs of the Four Colour Theorem. that transparently illustrates why four colours suffice to chromatically differentiate any set of contiguous, simply connected and bounded, planar spaces; by showing that:
-
(1)
If, for some natural numbers , every planar map of less than contiguous, simply connected and bounded, areas can be -coloured;
-
(2)
And, we assume (Hypothesis 1) that there is a sub-minimal -coloured planar map , of such areas, where finitary creation of a specific, additional, contiguous, simply connected and bounded, area within yields a minimal map which entails that require a 5th colour;
- (3)
Moreover we show why—challenging deep-seated dogmas that seemingly yet await, even if not actively seek, a mathematically ‘insightful’, and philosophically ‘satisfying’, proof of 4CT within inherited paradigms—the pictorial proof cannot be expressed within classical graph theory.
1.1 A historical perspective
It would probably be a fair assessment that the mathematical significance of any new proof of the Four Colour Theorem 4CT continues to be perceived as lying not in any ensuing theoretical or practical utility of the Theorem per se, but in whether the proof can address the philosophically ‘unsatisfying’, and occasionally ‘despairing’ (see [Tym79]; [Sw80]; [Gnt08], [Cl01]), lack of mathematical ‘insight’, ‘simplicity’, and ‘elegance’ in currently known proofs of the Theorem (eg. [AH77], [AHK77], [RSST], [Gnt08])—an insight and simplicity this investigation seeks in a pre-formal333The need for distinguishing between belief-based ‘informal’, and evidence-based ‘pre-formal’, reasoning is addressed by Markus Pantsar in [Pan09]; see also [An21], §1.D. proof of 4CT.
For instance we note—amongst others—some candid comments from Robertson, Sanders, Seymour, and Thomas’s 1995-dated (apparently pre-publication) summary444See [RSSp]; also [Thm98], [Cl01], and the survey [Rgrs] by Leo Rogers. of their proof [RSST]:
“Why a new proof?
There are two reasons why the Appel-Haken proof is not completely satisfactory.
Part of the Appel-Haken proof uses a computer, and cannot be verified by hand, and
even the part that is supposedly hand-checkable is extraordinarily complicated and tedious, and as far as we know, no one has verified it in its entirety.” …Robertson et al: [RSSp], Pre-publication.
“It has been known since 1913 that every minimal counterexample to the Four Color Theorem is an internally six-connected triangulation. In the second part of the proof, published in [4, p. 432], Robertson et al. proved that at least one of the 633 configurations appears in every internally six-connected planar triangulation. This condition is called “unavoidability,” and uses the discharging method, first suggested by Heesch. Here, the proof differs from that of Appel and Haken in that it relies far less on computer calculation. Nevertheless, parts of the proof still cannot be verified by a human. The search continues for a computer-free proof of the Four Color Theorem.” …Brun: [Bru02], §1. Introduction (Article for undergraduates)
“The four-colour problem had a long life before it eventually became the four-colour theorem. In 1852 Francis Gutherie (later Professor of Mathematics at the University of Cape Town) noticed that a map of the counties of England could be coloured using only four colours. He wondered if four colours would always suffice for any map. He, or his brother Frederick, proposed the problem to Augustus De Morgan (see the box at the end of Section 3.5 in Chapter 3) who liked it and suggested it to other mathematicians. Interest in the problem increased after Arthur Cayley presented it to the London Mathematical Society in 1878 ([Cay79]). The next year Alfred Bray Kempe (a British lawyer) gave a proof of the conjecture. His proof models the problem in terms of graphs and breaks it up into a number of necessary cases to be checked. Another proof was given by Peter Tait in 1880. It seemed that the four-colour problem had been settled in the affirmative.
However, in 1890 Percy John Heawood found that Kempe’s proof missed one crucial case, but that the approach could still be used to prove that five colours are sufficient to colour any map. In the following year Tait’s proof was also shown to be flawed, this time by Julius Petersen, after whom the Petersen graph is named. The four-colour problem was therefore again open, and would remain so for the next 86 years. In that time it attracted a lot of attention from professional mathematicians and good (and not so good) amateurs alike. In the words of Underwood Dudley:
The four-color conjecture was easy to state and easy to understand, no large amount of technical mathematics is needed to attack it, and errors in proposed proofs are hard to see, even for professionals; what an ideal combination to attract cranks!
The four-colour theorem was finally proved in 1976 by Kenneth Appel and Wolfgang Haken at the University of Illinois. They reduced the problem to a large number of cases, which were then checked by computer. This was the first mathematical proof that needed computer assistance. In 1997 N. Robertson, D.P. Sanders, P.D. Seymour and R. Thomas published a refinement of Appel [and] Haken’s proof, which reduces the number of necessary cases, but which still relies on computer assistance. The search is still on for a short proof that does not require a computer.” …Conradie/Goranko: [CG15], §7.7.1, Graph Colourings, p.417.
“The first example concerns a notorious problem within the philosophy of mathematics, namely the acceptability of computer-generated proofs or proofs that can only be checked by a computer; for instance because it includes the verification of an excessively large set of cases. The text-book example of such a mathematical result is the proof of the 4-colour theorem, which continues to preoccupy philosophers of mathematics (Calude 2001). Here, we only need to note that the debate does not primarily concern the correctness of the result, but rather its failure to adhere to the standard of surveyability to which mathematical proofs should conform.” …Allo: [All17], Conclusion, p.562.
“Being the first ever proof to be achieved with substantial help of a computer, it has raised questions to what a proof really is. Many mathematicians remain sceptical about the nature of this proof due to the involvement of a computer. With the possibility of a computing error, they do not feel comfortable relying on a machine to do their work as they would be if it were a simple pen-and-paper proof.
The controversy lies not so much on whether or not the proof is valid but rather whether the proof is a valid proof. To mathematicians, it is as important to understand why something is correct as it is finding the solution. They hate that there is no way of knowing how a computer reasons. Since a computer runs programs as they are fed into it, designed to tackle a problem in a particular way, it is likely they will return what the programmer wants to find leaving out any other possible outcomes outside the bracket.
Many mathematicians continue to search for a better proof to the problem. They prefer to think that the Four Colour problem has not been solved and that one day someone will come up with a simple completely hand checkable proof to the problem.” …Nanjwenge: [Nnj18], Chapter 8, Discussion (Student Thesis).
“The heavy reliance on computers in Appel and Haken’s proof was immediately a topic of discussion and concern in the mathematical community. The issue was the fact that no individual could check the proof; of special concern was the reductibility [sic] part of the proof because the details were “hidden” inside the computer. Though it isn’t so much the validity of the result, but the understanding of the proof. Appel himself commented: “…there were people who said, ‘This is terrible mathematics, because mathematics should be clean and elegant,’ and I would agree. It would be nicer to have clean and elegant proofs.” See page 222 of Wilson.” …Gardner: [Grd21], §11.1, Colourings of Planar Maps, pp.6-7 (Lecture notes).
2 A pictorial proof of the 4-Colour Theorem
We consider the surface of the hemisphere (minimal planar map ) in Fig.1 where:
-
1.
denotes a region of contiguous, simply connected and bounded, surface areas , none of which share a non-zero boundary segment with the contiguous, simply connected, surface area (as indicated by the red barrier which, however, is not to be treated as a boundary of the region );
-
2.
denotes a region of contiguous, simply connected and bounded, surface areas , some of which, say , share at least one non-zero boundary segment of with ; where, for each , for some ;
- 3.
Hypothesis 1 (Minimality Hypothesis)
Since four colours suffice for maps with fewer than 5 regions, we assume the existence of some , in a putatively minimal planar map , which defines a minimal configuration of the region where:
-
(a)
any configuration of contiguous, simply connected and bounded, areas can be -coloured if , where , and ;
-
(b)
any configuration of the contiguous, simply connected and bounded, areas of the region, say , in a putative, sub-minimal, planar map before the creation of —constructed finitarily by sub-dividing and annexing some portions from each area, say , of in —can be 4-coloured;
-
(c)
the region in the planar map is a specific configuration of contiguous, simply connected and bounded, areas that cannot be 4-coloured (whence the area necessarily requires a 5th colour by the Minimality Hypothesis).
Theorem 21 (Four Colour Theorem)
No planar map needs more than four colours.
Proof 22.
If the area of the minimal planar map in Fig.1 is divided further (as indicated in Fig.2) into two non-empty areas and , where:
-
•
shares a non-zero boundary segment with only one of the areas ; and
-
•
can be treated as an original area of in (see Hypothesis 1(b)) that was annexed to form part of in (in Fig.1);
then can be absorbed back into without violating the Minimality Hypothesis. Moreover, must share a non-zero boundary with in if for some , and are required to be differently coloured, in .
Such a division, as illustrated in Fig.2, followed by re-absorption of into (denoted, say, by ), would reduce the configuration in Fig.2 again to a minimal planar map, say with a configuration , where ; which would in turn necessitate a 5th colour for the area by the Minimality Hypothesis.
Since we cannot, by reiteration, have a non-terminating sequence , the sequence must terminate in a non-empty area of a minimal planar map, say , for some finite integer ; where contains no area that is annexed from any of the areas of in prior to the formation of the minimal planar map (in Fig.1).
Comment: Note that we cannot admit as a putative limit of the configuration where all the —corresponding to the abutting areas of in the Minimal Planar Map —meet at a point in the putative, sub-minimal, planar map , since any finitary (i.e., not postulated) creation of , begun by initially annexing a non-empty area of some at such an apex (corresponding to the putative ‘finally merged’ area of the above non-terminating sequence ), would require, at most, a 4th but not a 5th colour.
However, by Hypothesis 1(b), this contradicts the definition of the area , in the minimal planar map (in Fig.1)—ergo of the area in the minimal planar map —as formed finitarily by sub-division and annexation of existing areas of in .
Hence there can be no minimal planar map which defines a minimal configuration such as the region in Fig.1. The theorem follows.
We conclude by noting that, since classical graph theory555See, for instance, Brun [Bru02], Conradie/Goranko [CG15], Gardner [Grd21]. represents non-empty areas as points (vertices), and a non-zero boundary between two areas as a line (edge) joining two points (vertices), it cannot express the proof of Theorem 21 graphically.
Reason: The proof of Theorem 21 appeals to finitarily distinguishable properties of a series of, putatively minimal, planar maps , created by a corresponding sequence of areas where each area is finitarily created from, or as a proper subset of, some preceding area/s in such a way that the graphs of remain undistinguished.
References
-
[AH77]
Kenneth Appel and Wolfgang Haken. 1977. Every planar map is four colorable. Part I: Discharging. Illinois Journal of Mathematics, Volume 21, Issue 3 (1977), pp. 429-490, University of Illinois, Urbana-Champaign.
http://projecteuclid.org/download/pdf_1/euclid.ijm/1256049011 -
[AHK77]
Kenneth Appel, Wolfgang Haken and John Koch. 1977. Every planar map is four colorable. Part II: Reducibility. Illinois Journal of Mathematics, Volume 21, Issue 3 (1977), 491-567, University of Illinois, Urbana-Champaign.
http://projecteuclid.org/download/pdf_1/euclid.ijm/1256049012 -
[All17]
Patrick Allo. 2017. A Constructionist Philosophy of Logic. In Minds & Machines, 27, 545–564 (2017). https://doi.org/10.1007/s11023-017-9430-9
https://link.springer.com/article/10.1007/s11023-017-9430-9#Sec4 -
[An21]
Bhupinder Singh Anand. 2021. The Significance of Evidence-based Reasoning in Mathematics, Mathematics Education, Philosophy, and the Natural Sciences. Second edition, 2022 (Forthcoming). Limited First (Print) Edition archived at PhilPapers here.
https://philpapers.org/rec/ANATSO-4 -
[Bru02]
Yuriy Brun. 2002. The four-color theorem. In Undergraduate Journal of Mathematics, May 2002, pp.21–28. MIT Department of Mathematics, Cambridge, Massachussets, USA.
http://people.cs.umass.edu/brun/pubs/pubs/Brun02four-color.pdf -
[Cay79]
Arthur Cayley. 1879. On the Colouring of Maps. Proceedings of the Royal Geographical Society and Monthly Record of Geography, New Monthly Series, Vol. 1, No. 4 (Apr., 1879).
https://www.jstor.org/stable/1799998?refreqid=excelsior%3A8d25e3714824dadf86c153af680dc565&seq=1 -
[CG15]
Willem Conradie and Valentin Goranko. 2015. Logic and Discrete Mathematics: A Concise Introduction. First edition, 2015. John Wiley and Sons Ltd., Sussex, United Kingdom.
https://bcs.wiley.com/he-bcs/Books?action=index&bcsId=9628&itemId=1118751272 -
[Cl01]
Andreea S. Calude. 2001. The Journey of the Four Colour Theorem Through Time. The New Zealand Mathematics Magazine, 2001, 38:3:27-35, Auckland, New Zealand.
https://www.calude.net/andreea/4CT.pdf -
[Gnt08]
Georges Gonthier. 2008. Formal Proof—The Four Color Theorem. Notices of the AMS, December 2008, Volume 55, Number 11, pp.1382-1393.
http://www.ams.org/notices/200811/tx081101382p.pdf -
[Grd21]
Robert Gardner. 2021. The Four-Colour Problem. Lecture notes on Graph Theory 1, Fall 2020 (Revised 17/01/2021), Department of Mathematics and Statistics, East Tennessee State University, Johnson City, Indiana, USA.
https://faculty.etsu.edu/gardnerr/5340/notes-Bondy-Murty-GT/Bondy-Murty-GT-11-1.pdf -
[Nnj18]
Sean Evans Nanjwenge. 2018. The Four Colour Theorem. Thesis (Basic level: degree of Bachelor), Linnaeus University, Faculty of Technology, Department of Mathematics, Växjö, Sweden.
http://lnu.diva-portal.org/smash/get/diva2:1213548/FULLTEXT01.pdf -
[Pan09]
Markus Pantsar. 2009. Truth, Proof and Gödelian Arguments: A Defence of Tarskian Truth in Mathematics. In Eds. Marjaana Kopperi, Panu Raatikainen, Petri Ylikoski, and Bernt Österman, Philosophical Studies from the University of Helsinki 23, Department of Philosophy, University of Helsinki, Finland.
https://helda.helsinki.fi/bitstream/handle/10138/19432/truthpro.pdf?sequence=2 -
[Rgrs]
Leo Rogers. 2011. The Four Colour Theorem. Survey for 11-16 year olds on the University of Cambridge’s Millenium Mathematics Project weblog ‘NRICH’.
https://nrich.maths.org/6291 -
[RSSp]
Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas. 1995. The four-colour theorem. Pre-publication summary of [RSST].
http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.math.gatech.edu/ thomas/FC/fourcolor.html -
[RSST]
… 1997. The four-colour theorem. In the Journal of Combinatorial Theory, Series B, Volume 70, Issue 1, May 1997, Pages 2-44.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.137.9439&rep=rep1&type=pdf - [St81] Ian Nicholas Stewart. 1981. Concept’s of Modern Mathematics. 1981 ed. (paperback), Penguin Books, England.
-
[Sw80]
E. R. Swart. 1980. The Philosophical Implications of the Four-Color Problem. The American Mathematical Monthly, Vol. 87, No. 9 (Nov., 1980), pp. 697-707.
https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/Swart697-707.pdf -
[Thm98]
Robin Thomas. 1998. An Update On The Four-Color Theorem. Notices of The American Mathematical Society, Volume 45 (1998), no. 7, pp.848–859.
http://www.ams.org/notices/199807/thomas.pdf - [Tym79] Thomas Tymoczko. 1979. The Four-Color Problem and Its Philosophical Significance. The Journal of Philosophy, Vol. 76, No. 2. (Feb., 1979), pp. 57-83.