Het vierkleurenprobleem werd in 1852 opgeworpen door Francis Guthrie, en sindsdien proberen wiskundigen met de hand en met de computer te bewijzen dat vier kleuren altijd genoeg is. Niet iedereen was overtuigd van al die computerbewijzen. Wie weet er namelijk zeker of er niet ergens een fout in de code zit? Georges Gonthier liet er een tweede computer op los en toonde aan dat het vierkleurenbewijs wel snor zit.

Computerbewijzen

In 1976 werd door Kenneth Appel en Wolfgang Haken een bewijs geleverd dat gebruik maakt van de computer, waarin zo’n 1500 ‘configuraties’ onderzocht werden, ieder leidend tot duizenden gevallen. Sceptici keurden dit computerbewijs af, omdat ze niet vertrouwden op de berekeningen die de computer maakte.

Sinds 1994 is er een tweede vierkleurenbewijs (van Neil Robertson en anderen), dat eveneens gebruik maakt van de computer. In dit bewijs is het aantal configuraties teruggebracht tot 633 en werd de complexiteit van de controleper configuratie teruggebracht. Maar ook toen ontstond er discussie over de betrouwbaarheid van de nog steeds omvangrijke computerberekeningen. Misschien dat aan die discussie nu een eind komt. In december 2004 namelijk presenteerde Georges Gonthier op een conferentie in Jouy-en-Josas (nabij Parijs) een versie van Robertsons bewijs, die zo nauwkeurig uitgeschreven is dat de juistheid van elke stap gecontroleerd kon worden. Die controle werd uitgevoerd door de ‘bewijs-assistent’ Coq: een programma van Franse origine, dat de juistheid van wiskundige bewijzen verifieert.