QED

De vierkleurenstelling is het bekendste voorbeeld van een stelling die met behulp van een computer is bewezen. In 1976 bewezen de wiskundigen Kenneth Appel en Wolfgang Haken met behulp van uitgebreide computerberekeningen de vierkleurenstelling: voor een willekeurige landkaart is het mogelijk om de landen met hoogstens vier kleuren zò in te kleuren dat geen twee aangrenzende landen dezelfde kleur hebben. We noemen twee landen aangrenzend als ze een grens delen; landen die slechts in een punt aan elkaar liggen (zoals twee overliggende spieën van een gesneden taart) zijn dus niet aangrenzend. Met een land bedoelen we bovendien een samenhangend deel van de kaart.

De bekendheid van de vierkleurenstelling overschaduwt echter heel wat andere computerbewijzen, zelfs zo erg dat het bewijs van Appel en Haken vaak het eerste computerbewijs genoemd wordt. Ik geef hier enkele voorbeelden waar dit beweerd wordt. Arnout Jaspers schrijft in het januarinummer van Pythagoras een kort artikel over de vierkleurenstelling. Over de prestatie van Appel en Haken schrijft hij:

Ze gebruikten toen als eersten een computer bij een bewijs.

Michelle Beard schrijft in een paper:

More importantly, The Four Color Theorem has changed the way that mathematical proof is viewed. The Four Color Theorem is the first proof that used a computer and was not actually able to be verified by hand.

In een interview met de bekende wiskundige Ian Stewart vraagt de interviewer:

You were a group theorist in the days of the Appel-Haken proof of the classification of simple groups in 1976. Can you give us a first-hand account of the reactions of the mathematical community to the first computer-assisted proof in history?

Ik negeer hier even het feit dat de interviewer de classificatie van eenvoudige groepen verwart met het vierkleurenprobleem, maar ook hier weer zien we het vooroordeel dat het bewijs van Appel en Haken het eerste computerbewijs was. Stewart reageert niet eens op de twee fouten in de vraag. In een tijdlijn van de geschiedenis van de wiskunde, door Qinfeng Huang van Washington University, lezen we bij 1976:

First computer assisted proof: Guthrie’s four color map problem.

Anderen zijn correcter in hun bewoordingen, maar vaak in zo’n subtiele verwoordingen dat de niet zo aandachtige lezer zou kunnen denken dat het bewijs van Appel en Haken toch het eerste computerbewijs is. Zo schrijven John J O’Connor en Edmund F Robertson van het MacTutor History of Mathematics archief van de University of St Andrews:

The Four Colour Theorem was the first major theorem to be proved using a computer, having a proof that could not be verified directly by other mathematicians.

Ook de Wikipedia-pagina gebruikt dezelfde vermelding, “the first major theorem”:

The four color theorem was the first major theorem to be proven using a computer, and the proof is not accepted by all mathematicians because it would be unfeasible for a human to verify by hand (see computer-assisted proof).

Ze hebben gelijk dat de vierkleurenstelling de eerste grote stelling is die met behulp van een computer bewezen is, maar dat woordje wordt vaak over het hoofd gezien. De bewering dat het bewijs van Appel en Haken het eerste wiskundig bewijs was waarvoor een computer nodig was, is blijkbaar een stevig verankerde mythe geworden. Heel wat wiskundeliefhebbers nemen dat vooroordeel dan over op hun homepage en kopiëren de mythe (bijvoorbeeld hier en hier).

Wat was dan wel het eerste computerbewijs van een nieuwe stelling? Volgens mij komt de eer toe aan de befaamde getaltheoreticus Derrick Lehmer, die ook nog meegewerkt heeft aan de Eniac-computer. Er waren al kleine priemgetallen van de vorm 6m + 1 bekend die geen drie opeenvolgende kubische residu’s hebben, en deze werden uitzonderlijke priemgetallen genoemd. Sinds 1928 was al bekend dat alle “voldoende grote” priemgetallen van de vorm 6m + 1 drie opeenvolgende kubische residu’s hebben. Dit betekende dus dat er maar een eindig aantal uitzonderlijke priemgetallen bestaan. Lehmer vond in 1962 met een computer alle uitzonderlijke priemgetallen en bewees (eveneens met een computerprogramma) dat de opeenvolgende kubische residu’s van alle niet-uitzonderlijke priemgetallen kleiner dan 23535 zijn. De publicatie: Derrick Henry Lehmer, Emma Lehmer, W. H. Mills en John L. Selfridge, “Machine proof of a theorem on cubic residues”, Mathematics of computation, Vol. 16, No. 80 (oktober 1962), pp. 407-415, online te vinden op JSTOR voor wie toegang heeft.

Addendum: ook Ursula Martin noemt in haar artikel “Computers, reasoning and mathematical practice” (1999) het bewijs van Appel en Haken het eerste computerbewijs: “The proof of the four colour theorem by Appel and Haken in 1977 was the earliest and most famous use of a computer in a proof.”