Wiskundigen vinden fout in een zestig jaar oud bewijs

In dit artikel:

Wiskundigen hebben een fout ontdekt in een cruciaal bewijs dat ten grondslag ligt aan de kristallijne cohomologie, een belangrijke tak van de moderne wiskunde. Deze ontdekking deed zich voor tijdens een project dat tot doel heeft wiskunde toegankelijk te maken voor computers, wat kan helpen bij het opsporen van foutieve aannames in historische bewijzen. Het probleem werd blootgelegd door Antoine Chambert-Loir van de Université Paris Cité toen hij het bewijs van Norbert Roby uit 1965 verwerkte in een computerleesbare taal.

Gelukkig bleek de fout te herstellen, dankzij aanvullend werk van Brian Conrad van Stanford, wat betekende dat de basis van de kristallijne cohomologie niet in gevaar was. Het incident benadrukt echter de noodzaak van formalisatie; door het vertalen van wiskundige bewijzen kunnen potentiële fouten in de grote hoeveelheid academische literatuur waarin dergelijke bewijzen zijn gepresenteerd, aan het licht komen. Chris Birkbeck en Chris Williams, beide wiskundigen, wijzen erop dat het essentieel is om de integriteit van oude en complexe bewijsvoering te waarborgen, gezien de implicaties voor talrijke andere wiskundige werken. Er bestaat consensus dat formalisatie een effectieve manier biedt om deze zorg te adresseren en zo de fundamenten van de wiskunde te versterken.