Al meer dan tien jaar is de wiskundige gemeenschap verwikkeld in een fel debat over de geldigheid van een grootschalig, controversieel bewijs. Nu biedt een nieuwe technologische grens –computerondersteunde formalisering —een mogelijke manier om het geschil eindelijk op te lossen.
De controverse over het ABC-vermoeden
Het conflict draait om het ABC-vermoeden, een fundamenteel probleem dat betrekking heeft op de relatie tussen optelling en vermenigvuldiging van priemgetallen. In 2012 publiceerde Shinichi Mochizuki van de Universiteit van Kyoto een bewijs van 500 pagina’s dat beweerde deze al lang bestaande puzzel op te lossen.
Zijn methode – een complex raamwerk genaamd de Inter-universele Teichmüller (IUT)-theorie – was echter zo ongekend dat de mondiale wiskundige gemeenschap hierdoor verdeeld bleef. Terwijl Mochizuki en zijn aanhangers volhouden dat het bewijs juist is, hebben veel vooraanstaande wiskundigen, waaronder Peter Scholze en Jakob Stix, betoogd dat de logica een fatale fout bevat.
Deze impasse heeft geleid tot een zeldzame ‘patstelling’ in de moderne wetenschap: de ene kant ziet een baanbrekende waarheid, terwijl de andere kant een niet te ontcijferen of gebroken argument ziet.
De opkomst van formalisering
Om deze impasse te doorbreken wenden onderzoekers zich tot Lean, een gespecialiseerde programmeertaal die is ontworpen voor ‘formalisering’. In dit proces worden wiskundige bewijzen vertaald in code die een computer met absolute logische zekerheid kan verifiëren. Hierdoor wordt het ‘menselijke element’ – het potentieel voor misverstanden, sociale druk of vooringenomenheid door peer review – verwijderd en vervangen door binaire waarheid.
Twee verschillende projecten proberen momenteel deze technologie te gebruiken om de kwestie op te lossen:
1. Het LANA-project (de zoektocht naar waarheid)
Onder leiding van Kato Fumiharu van het ZEN Mathematics Center heeft het Lean and Anabelian meetkunde (LANA) project tot doel het bewijs voor eens en voor altijd te verifiëren. Deze groep bestaat uit experts in zowel de specifieke theorieën van Mochizuki als de Lean programmeertaal.
Ondanks hun vooruitgang stuitte het project op een aanzienlijke wegversperring. Ze hebben een specifiek, problematisch punt in de IUT-theorie geïdentificeerd dat de fout weerspiegelt die Scholze en Stix in 2018 hebben geïdentificeerd. Na achttien maanden intensief onderzoek blijft het team steken in deze specifieke logische knoop.
2. Mochizuki’s project (de zoektocht naar duidelijkheid)
Op een andere manier zijn Mochizuki en zijn collega’s ook begonnen met het formaliseren van zijn werk in Lean. Hun doel is echter niet om hun eigen juistheid te ‘bewijzen’ – omdat ze denken dat die al bewezen is – maar om de code te gebruiken als een precies communicatiemiddel.
Mochizuki stelt dat Lean een ‘precies verslag’ zal maken van zijn logische structuur, waardoor deze immuun wordt voor de verkeerde interpretaties die de controverse jarenlang hebben aangewakkerd. Hoewel zijn team de eerste 70 regels code heeft geproduceerd, merken experts op dat dit nog maar het begin is van wat waarschijnlijk een monumentale taak zal zijn.
Waarom dit belangrijk is
De oplossing van het ABC-vermoeden gaat over meer dan slechts één vergelijking; het vertegenwoordigt een keerpunt in de manier waarop wiskunde wordt beoefend.
- De validatiecrisis: Als de computer een fout ontdekt, zal hij een decennium van academische wrijving oplossen.
- De nieuwe methodologie: Als het bewijs wordt geverifieerd, bewijst het dat ‘formalisering’ een haalbare manier is om met steeds complexere wiskundige ideeën om te gaan die de menselijke cognitieve grenzen overschrijden.
- De Communicatiebrug: De dialoog tussen het LANA-project en de groep van Mochizuki suggereert dat technologie eindelijk een gemeenschappelijke taal zou kunnen bieden voor wiskundigen die anders niet in staat zouden zijn geweest effectief te communiceren.
Conclusie
Hoewel de technische hindernissen enorm blijven, vertegenwoordigt de verschuiving naar computer-geverifieerde wiskunde de eerste echte beweging in de ABC-controverse in jaren. Of de code het werk van Mochizuki nu bevestigt of corrigeert, het resultaat zal de manier waarop wiskundige waarheid wordt vastgesteld en gecommuniceerd fundamenteel veranderen.
