Door een technische fout is er bij het artikel 'QED per pc – het nieuwe bewijzen' een kolom tekst weggevallen op pagina 59. Graag bieden we u de ontbrekende tekstkolom alsnog:


…rekenwerk kostte (zie kader, puzzel met de vier kleuren).
Maar al meteen was het bewijs omstreden. Door mensen was het computerbewijs immers onmogelijk na te kijken, omdat niemand met zekerheid kon zeggen of er niet een fout in de code zat. Veel wiskundigen waren er dan ook niet van overtuigd dat de vierkleurenstelling bewezen was. Maar in 2004 bewees de Franse informaticus Georges Gonthier met een bewijsverificatieprogramma alsnog dat het bewijs correct is. Coq, heet dat programma dat Gonthier gebruikte. En Coq geldt steeds meer als dé 'bewijsassistent' in de wiskunde.
Coq is wezenlijk dan ook anders dan het computerprogramma dat Appel en Haken gebruikten. Allereerst is Coq een algemeen programma, dat wordt gebruikt om allerlei verschillende, wiskundige bewijzen te controleren. Fouten in Coq zelf zouden bij de eenvoudigere problemen al snel aan het licht komen – vandaar dat het programma geldt als betrouwbaar werkpaard. Coq gebruikt een aantal axioma's, logische regels om nieuwe beweringen uit af te leiden, en een grote basisbibliotheek van stellingen die al eerder bewezen zijn.
Nu hoeven mensen alleen nog het systeem Coq te controleren. Ook Coq vergt immers nog enig vertrouwen van de wiskundige die van hem gebruikmaakt. Allereerst moet die erop vertrouwen dat het logische systeem achter Coq consistent is; een kwestie die voor deelsystemen al is bewezen. Voorts moet men vertrouwen op de implementatie en de compiler, het gedeelte dat de invoer vertaalt naar uitvoer. Het goede nieuws op dit punt is dat Coqs compiler voor zoveel verschillende toepassingen en ook andere software is gebruikt, dat het onwaarschijnlijk is dat er nog een fout in zit die de werking van Coq verpest. Dan is er nog de kernel van Coq, de centrale 'taakverdeler' in het programma. Die is bewust klein gehouden, om de kans op fouten te minimaliseren. Tenslotte moet de gebruiker op zijn hardware kunnen vertrouwen. Wiskundigen laten Coq daarom soms voor de zekerheid op een paar verschillende machines draaien.
Voor Gonthier was Coq in elk geval een verademing. Om het bewijs van de vierkleurenstelling te controleren, hoefde hij alleen maar de gebruikte definities en de formulering van Appel en Hakens programma na te kijken, bij elkaar ongeveer 250