QED

Het decembernummer van de Notices of the American Mathematical Society heeft als thema “formal proof”, met artikels over door computers gegenereerde en door computers geverifieerde bewijzen. De volgende vier artikels van experts geven een overzicht van de nieuwste ontwikkeling in het domein van formele bewijzen en de computertools daarvoor:

• Formal Proof, door Thomas Hales, University of Pittsburgh
• Formal proof—The Four Colour Theorem, door Georges Gonthier, Microsoft Research, Cambridge, England
• Formal Proof—Theory and Practice, door John Harrison, Intel Corporation
• Formal Proof—Getting Started, door Freek Wiedijk, Radboud University, Nijmegen, Netherlands

Wanneer wiskundigen op de traditionele manier een stelling bewijzen, doen ze dat in een mengeling van (vaak) Engels en wiskundige symbolen. Ze verwijzen daarbij naar vroegere resultaten, laten details open die als “triviaal” beschouwd worden en doen vaak een beroep op intuïtie. De correctheid van zo’n bewijzen wordt bepaald door referees en andere wiskundigen die de argumenten nalezen of erover discussiëren. Dit is in essentie een sociaal proces. Meestal werkt dit, maar er zijn verschillende voorbeelden van foute resultaten die lang als correct werden beschouwd, zoals Alfred Bray Kempe’s ‘bewijs’ in 1879 van de vierkleurenstelling, waarin pas in 1890 een fatale fout ontdekt werd.

De twintigste eeuw kende bovendien een explosie van wiskunde en ook een explosie van complexe bewijzen die honderden of duizenden pagina’s innemen. Sommige van deze bewijzen zijn bovendien gebaseerd op ellenlange berekeningen op een computer, samen met ingewikkelde computercode. Dit soort bewijzen is een grote uitdaging voor wiskundigen, want de correctheid hiervan is in de praktijk niet na te gaan. Je mag wel stellen dat de kans dat zo’n complex bewijs geen fout bevat
onbestaande is.

Om deze uitdagingen aan te kunnen gaan, hebben een aantal computerwetenschappers en wiskundigen computertools ontwikkeld die volledig formele bewijzen helpen opstellen, waarvan elke logische stap automatisch kan gecontroleerd worden om de correctheid voor eens en voor altijd na te gaan. Sommige van deze computerprogramma’s kunnen ook zelf proberen om een bewijs van een opgegeven stelling te maken en gaan dan zelf op zoek naar de nodige tussenstappen. Voor eenvoudige stellingen lukt dit al. Als deze programma’s in de toekomst verbeteren, zouden we van alle belangrijke stellingen in de wiskunde een formeel bewijs kunnen leveren, dat volgens wiskundige Thomas Hales dan zoiets zou vormen als “the sequencing of the mathematical genome”.

Wie controleert de controleurs?

Maar als je bewijzen laat controleren door computerprogramma’s, wie bewijst dan dat die computerprogramma’s wel correct hun werk doen? Hales geeft in zijn artikel een anekdotisch voorbeeld van waar het fout kan gaan, en waarom hij denkt dat dit geen probleem is bij gebruik van een bekend bewijsprogramma:

Experience from other top-tier theorem-proving systems [than HOL Light] has been that about three to five bugs have been found in each system over a period of 15-20 years of use. After decades of use on many different systems, to my knowledge, only one proof has ever had to be retracted as a result of a bug in a theorem-proving system, and this in a system that I do not rank in the top-tier: in 1995 a heap overflow error led to the false claim that the theorem-prover REVEAL had solved the Robbins conjecture. We can assert with utmost confidence that the error rates of top-tier theorem-proving systems are orders of magnitude lower than error rates in the most prestigious mathematical journals. Indeed, since a formal proof starts with a traditional proof, then does strictly more checking even at the human level, it would be hard for the outcome to be otherwise.

Hales is overigens degene die met behulp van computerberekeningen het Keplervermoeden bewezen heeft. Zijn bewijs werd door het prestigieuze tijdschrift The Annals of Mathematics met gemengde gevoelens ontvangen. Het duurde zo’n vijf jaar voordat het team van 12 (!) referees het bewijs gecontroleerd hadden. Het hoofd van het team referees, Gábor Fejes Tóth, zei dat ze 99% zeker waren van de correctheid van het bewijs, maar dat ze de correctheid van alle computerberekeningen niet konden garanderen omdat ze niet elke lijn computercode konden nakijken.

De editors van The Annals besloten om Hales’ bewijs in twee te splitsen: ze publiceerden enkel het theoretische gedeelte van het bewijs, dat op de traditionele manier door referees was nagekeken. Dit deel beschouwden ze als een correct en zelfs hoogstaand bewijs. Voor de publicatie van het computergedeelte moest Hales zijn toevlucht zoeken tot het gespecialiseerde tijdschrift Discrete and Computational Geometry. Mede door deze ervaring is Hales begonnen met het Flyspeck-project, een volledig formeel en door computers geverifieerd bewijs van het Keplervermoeden. Hij vermoedt dat dit zo’n twintig manjaren zal vereisen.

Op Kennislink kan je een uitgebreidere versie van dit artikel lezen.