Een controversieel bewijs in de wiskunde – een bewijs dat het veld al meer dan tien jaar verdeeld heeft – zou eindelijk door een onwaarschijnlijke rechter kunnen worden beslecht: een computerprogramma. De kern van het debat draait om de poging van Shinichi Mochizuki uit 2012 om het ABC-vermoeden op te lossen, een al lang bestaand probleem dat diep geworteld is in de fundamentele aard van getallen.
Het ABC-vermoeden draait om een bedrieglijk eenvoudige vergelijking met drie gehele getallen: a + b = c. Het stelt specifieke regels die bepalen hoe priemgetallen waaruit deze gehele getallen bestaan, zich moeten verhouden. Het oplossen van dit ogenschijnlijk fundamentele probleem zou diepgaande inzichten in de wiskunde kunnen opleveren, wat mogelijk van invloed kan zijn op andere beroemde vermoedens zoals de Laatste Stelling van Fermat.
Mochizuki, een professor aan de Universiteit van Kyoto in Japan, presenteerde zijn bewijs binnen een complex raamwerk dat hij had uitgevonden, de interuniversele Teichmüller-theorie (IUT). Het louter technische karakter en de onduidelijkheid van de IUT-theorie maakten deze echter grotendeels onbegrijpelijk voor de meeste wiskundigen die zijn werk probeerden te verifiëren. Het aanvankelijke enthousiasme maakte plaats voor frustratie toen experts moeite hadden om de fijne kneepjes ervan te ontcijferen.
Om olie op het vuur te gooien, ontdekten twee vooraanstaande Duitse wiskundigen – Peter Scholze en Jakob Stix – in 2018 een mogelijke fout in het bewijs van Mochizuki. Mochizuki weerlegde hun argument, en zonder een overkoepelend orgaan dat wiskundige geschillen beslechtte, viel het veld in twee kampen uiteen: degenen die grotendeels de mainstream-visie accepteerden (ondersteund door de meeste wiskundigen) en een kleinere groep die zich aansloot bij Mochizuki en zijn instituut in Kyoto.
Nu stelt Mochizuki een weg voorwaarts voor via formalisering: hij zet zijn bewijs om van voor mensen leesbare wiskundige notatie naar Lean, een computerprogrammeertaal die speciaal is ontworpen voor rigoureuze wiskundige verificatie. Dit proces zou computers mogelijk in staat kunnen stellen automatisch de consistentie van zijn argumenten te controleren, wat een ongekend niveau van objectiviteit oplevert.
Mochizuki gelooft dat Lean op unieke wijze is toegerust om de complexe taalkundige en conceptuele hindernissen te overwinnen die de vooruitgang in het begrijpen van de IUT-theorie hebben tegengehouden. Hij beschouwt het als een instrument om de wiskundige waarheid te bevrijden van de potentiële vooroordelen die inherent zijn aan menselijke interpretatie.
Hoewel sommige experts, zoals Kevin Buzzard van het Imperial College London, dit als een veelbelovende richting zien, erkennen zij ook de enorme uitdaging die voor ons ligt. Het formaliseren van de IUT-theorie zou vereisen dat enorme hoeveelheden ingewikkelde vergelijkingen in de syntaxis van Lean worden vertaald – een onderneming die lijkt op enkele van de grootste formaliseringsprojecten die ooit zijn ondernomen. Bij dergelijke inspanningen zijn vaak toegewijde teams van wiskundigen en programmeurs betrokken die maanden of zelfs jaren duren.
Johan Commelin van de Universiteit Utrecht is weliswaar voorzichtig optimistisch, maar benadrukt dat succes afhangt van de aanhoudende inzet van Mochizuki. Hij waarschuwt dat als het project voortijdig wordt stopgezet, het eenvoudigweg een nieuw hoofdstuk kan worden in een langdurige saga die wordt gekenmerkt door onopgeloste geschillen.
Zelfs als dit lukt, wijst Commelin erop dat zelfs met computergeverifieerde code meningsverschillen over de interpretatie kunnen blijven bestaan. Lean kan logische tegenstrijdigheden oplossen, maar niet noodzakelijkerwijs alle filosofische of conceptuele verschillen rond Mochizuki’s werk onderdrukken.
Hoewel formalisering uiteindelijk een sprankje hoop biedt voor het oplossen van deze aanhoudende wiskundige impasse, valt het nog te bezien of het de diepgewortelde complexiteiten en verschillende perspectieven kan overwinnen die het debat over het ABC-vermoedensbewijs hebben gekenmerkt.
