Het Uiteindelijke Bewijs  
   
...HEESCH

Zo rond 1960 was men nog steeds druk aan 't zoeken naar onvermijdelijke verzamelingen van kaarten die allemaal verkleinbaar waren.
Heinrich Heesch was één van de grote figuren (o.a. de uitvinder van de methode van ontlading). De verzamelingen werden echter groter en groter.
Voor de Birkhoff-diamant (ring van grootte 6) waren 31 mogelijkheden, maar als de ringen groter worden neemt het aantal mogelijke kleuringen ervan ook spectaculair toe,  zoals je ziet in de volgende tabel:
   
ringgrootte 6 7 8 9 10 11 12 13 14
kleuringen 31 91 274 820 2461 7381 22144 64430 199291
   
Een ring van 18 zou al meer dan 18 miljoen mogelijke kleuringen hebben!!! 't Is ongeveer een factor 4 extra per land extra.
Typisch een werkje voor een computer dus.
En dus kwamen de computermensen ten tonele.....

...HAKEN

 
Wolfgang Haken woonde als student een lezing van Heesch bij, en was wel geïnteresseerd in het probleem. Hij was een stugge doorwerker, en had op het gebied van knopen-theorie al successen behaald door gewoon heel veel gevallen allemaal door te rekenen. Zoals iemand over hem opmerkte:

   
Wiskundigen weten meestal wanneer zij te diep het bos in zijn gegaan om nog verder te kunnen.
Maar dan komt Haken, en neemt zijn zakmes, en begint de bomen één voor één neer te halen....
   
Ze gaan samenwerken als Haken een veel betere ontladingsmethode vindt om kaarten zonder zes- of zevenhoeken te behandelen.
Nog steeds lopen hun pogingen echter vast op drie belangrijke kaarten:
   

   
Haken begon zijn aanpak te veranderen. Bijna iedereen was druk bezig verzamelingen van verkleinbare kaarten te maken. Als dat grote indrukwekkende verzamelingen waren probeerde men er een onvermijdelijke verzameling uit te destilleren.
Haken begon aan de andere kant. Hij concentreerde zich op onvermijdelijke verzamelingen, en als hij die had ging hij pas kijken of ze verkleinbaar waren. Hij koos vaak alvast kaarten die waarschijnlijk verkleinbaar zouden zijn. Bekende obstakels als hierboven liet hij niet toe. Deze aanpak scheelde een boel werk; hij hoefde niet van allerlei kaarten die hij toch niet ging gebruiken voor een onvermijdelijke verzameling aan te tonen dat ze verkleinbaar waren.
   
...APPEL  
   
Appel hoorde een lezing van Haken waarin hij de enorme rekenproblemen noemde. Nou was hij zelf een ervaren programmeur, en bood na afloop Haken aan met hem te gaan samenwerken. Dat deden ze vanaf 1972. Toen begonnen de jaren van rekenen pas écht.  Stapje voor stapje kwamen ze verder. Een kleine greep:
 
• In 1974 hadden ze bijvoorbeeld een verzameling van 47 figuren die samen een onvermijdelijke verzameling vormden en die allemaal verkleinbaar waren. Maar nog wel met de beperking dat er niet 2 vijfhoeken aan elkaar mogen grenzen.
• Ze moesten hun ontladingsmethode uitbreiden tot 487 verschillende ontlaadmanieren!
• Het berekenen van verkleinbaarheid bleek vaak een enorme taak.  Sommige figuren zouden een mens die 40 uur per week werkt in totaal 5 jaar werk kosten! Op een gegeven moment lieten ze een computer nog maar 90 minuten aan een figuur rekenen om verkleinbaarheid te testen. Als het dan niet gelukt was gooiden ze de figuur weg en probeerden hem te vervangen door anderen.
• De komst van een nieuwe, snellere computer bespaarde hen naar schatting zo'n 2 jaar aan verkleinbaarheid testen.
   
Eind juni 1976 was het eind in zicht. Het leek erop dat ze de gezochte onvermijdelijke verzameling hadden gevonden. Binnen 2 dagen had de computer inderdaad aangetoond dat alle figuren verkleinbaar waren. En toen begon het controleren.  Ook dat bleek nog een heel werk.
Ze lieten vijf van hun kinderen meehelpen met controleren. Dorothy en Armin Haken en Laurel, Peter en Andrew Appel moesten aan de slag. Laurel Haken nam bijvoorbeeld zo'n 700 pagina's voor haar rekening. Ze vond ongeveer één fout per pagina, meestal typefouten. Op 50 na wist ze ze allemaal te corrigeren. Herberekening van deze 50 liet nog 12 fouten over. Deze 12 werden vervangen door 20 nieuwe figuren, en zo ging het maar door en door en door.

22 juli 1976 konden ze eindelijk hun bewijs openbaar maken!
Op 23 juli stond het volgende bericht in  The Times:
   
Twee Amerikaanse wiskundigen hebben verklaard een probleem dat de wiskundewereld meer dan 100 jaar heeft beziggehouden te hebben opgelost. Hun bewijs, vandaag gepubliceerd, beslaat 100 pagina's samenvatting, 100 pagina's details, 700 pagina's bijlagen. Het kostte hen 40 uur onderzoek per week en 1000 uur computertijd. Hun bewijs bevat 10000 diagrammen en de computeruitdraai is zo'n anderhalve meter hoog...