Bij een project dat als doel heeft om wiskunde leesbaar te maken voor computers, ontdekten wiskundigen een fout in een belangrijk bewijs. Ze wisten de fout te herstellen, maar het incident illustreert dat er mogelijk meer fouten schuilgaan in oude wiskundige bewijzen.
De fout stond in een bewijs dat ten grondslag ligt aan een populaire tak van de moderne wiskunde. Hij kwam per toeval aan het licht toen wiskundigen oude bewijzen omschreven naar een taal die door computers kan worden gelezen. De fout werd snel hersteld, maar volgens wiskundigen onderstreept het voorval dat het belangrijk is om wiskunde leesbaar te maken voor machines, omdat dit vergelijkbare problemen kan blootleggen.
Machine controleert mens
De meeste wiskunde is te lezen in publicaties en lesboeken. Om ervoor te zorgen dat wat op papier staat correct is, controleren wiskundigen elkaars werk. Een bewijs is dus in de basis een sociale afspraak: als genoeg wiskundigen overtuigd zijn dat de logische stappen van een bewijs correct zijn, dan wordt het als waar beschouwd. In de zeldzame gevallen dat wiskundigen er niet uit komen, blijft de status van een bewijs in het ongewisse.
‘Einstein liep als theoreticus vast op de nieuwe bevindingen’
Toen de Nederlandse natuurkundige Heike Kamerlingh Onnes iets geks ontdekte over supergeleiding, was dit onder veel fysici het gesprek van de dag. Maa ...
Een manier om dit te voorkomen, is om bewijzen stap voor stap te laten controleren door een computer. Maar dit betekent wel dat die bewijzen vertaald moeten worden naar een voor machines leesbare taal. Dit proces heet formalisatie. Het vertalen voor een computercheck is een relatief nieuw idee en kan tijdrovend zijn.
Onlangs startte het team van wiskundige Kevin Buzzard van het Imperial College in Londen een ambitieus project: om het bewijs van de laatste stelling van Fermat te formaliseren. Dit bewijs, dat erg belangrijk is voor de moderne wiskunde, maakt gebruik van verschillende complexe takken van het vakgebied. Veel daarvan zijn nog niet machineleesbaar, dus moeten eerst worden vertaald.
Een van die takken is een onderdeel van de meetkunde, kristallijne cohomologie geheten. Tijdens het vertalen hiervan stuitte wiskundige Antoine Chambert-Loir van de Université Paris Cité op een probleem. Een deel van een oud bewijs dat de grondslag vormt van de kristallijne cohomologie bleek een fout te bevatten. Het bewijs is in 1965 geleverd door de Franse wiskundige Norbert Roby. Nu ontdekte Chambert-Loir dat Roby een symbool tussen twee regels was vergeten, waardoor zijn bewijs niet werkte.
Domino-effect
Als Roby’s werk het enige bewijs was geweest dat de kristallijne cohomologie correct is, zou dit foutje hebben geleid tot een domino-effect, waarbij veel recentere bewijzen die zich erop baseren om zouden vallen. Gelukkig is de kristallijne cohomologie sinds de jaren zestig op verschillende manieren bewezen, met verschillende strategieën. Het was Buzzard daarom wel duidelijk dat het bewijs hersteld kon worden.
Hij besprak de fout met collega’s. Daarop vond wiskundige Brian Conrad van de Stanford-universiteit in de VS een nieuwer bewijs dat ook de strategie van Roby volgde. Daaruit bleek dat Roby’s fout herstelbaar was. Daarmee bleef dit specifieke probleem binnen de perken. Maar de wiskundigen zien het als een voorbode van grotere fouten die misschien schuilgaan in de wiskundige literatuur, die meer impact op het vakgebied zullen hebben.
Nachtmerrie
Wiskundige Chris Birkbeck van de Universiteit van East Anglia in het Verenigd Koninkrijk noemt het verrassend dat zo’n veelgebruikt vakgebied als de kristallijne cohomologie gestoeld is op zulke obscure en lastig te vinden referenties. Hij zegt dat het formaliseren van de wiskunde zal helpen controleren of de berg academische literatuur die nu bestaat niet nog meer fouten bevat. ‘Wiskunde is behoorlijk ingewikkeld geworden. Het is onmogelijk om alles tot op het axioma (de geaccepteerde waarheid waarmee een bewijs begint, red.) door te lezen.’
‘Het idee dat een bewijs dat het fundament vormt van duizenden andere werken een fout kan bevatten, is een nachtmerrie’, zegt wiskundige Chris Williams van de Universiteit van Nottingham in het Verenigd Koninkrijk. ‘Formalisatie biedt op een andere manier zekerheid over de geldigheid van de fundamenten op ons vakgebied, en dat is zeer welkom.’
