En tioårig dispyt inom matematiken kring Shinichi Mochizukis bevis för ABC-konjekturen kan lösas med datorformalism. Mochizuki har föreslagit att översätta sitt 500-sidiga verk till programmeringsspråket Lean för automatisk verifiering. Detta tillvägagångssätt skulle kunna överbrygga skillnaderna mellan de motstridiga lägren i den matematiska gemenskapen.
Kontroversen går tillbaka till 2012, när Shinichi Mochizuki, professor vid Kyotos universitet i Japan, publicerade ett omfattande 500-sidigt bevis för ABC-konjekturen. Detta 40 år gamla problem rör ekvationen a + b = c för heltal och relationerna mellan deras primfaktorer, med implikationer för satser som Fermats sista sats. Mochizukis bevis bygger på hans intrikata inter-universella Teichmüller-teori (IUT), som många experter fann svår att tränga igenom.
Den initiala entusiasmens avtog när verifieringsförsöken stannade av. År 2018 identifierade Peter Scholze från Bonns universitet och Jakob Stix från Goethe-universitetet i Frankfurt en potentiell brist, som Mochizuki bestred. Utan en central myndighet delades matematikvärlden: de flesta matematiker på ena sidan, och en mindre grupp ansluten till Mochizuki och Kyotos forskningsinstitut för matematiska vetenskaper på den andra.
För att bryta dödläget förespråkar Mochizuki nu formalisering av beviset i Lean, ett språk för datorverifierad matematik. Inspirerad av en juli-konferens i Tokyo argumenterar han i en nylig rapport för att Lean skulle kunna befria matematisk sanning från "sociala och politiska dynamiker". Som han skriver: "[Lean] är den bästa och kanske enda tekniken… för att uppnå meningsfullt framsteg med avseende på det grundläggande målet att befria matematisk sanning från oket av sociala och politiska dynamiker."
Experter ser potential men varnar. Kevin Buzzard vid Imperial College London noterar: "Om det är skrivet i Lean, så är det inte galet, eller hur? Mycket av materialet i artiklarna är skrivet i ett mycket konstigt språk, men om du kan skriva det i Lean, betyder det åtminstone att det konstiga språket har blivit en helt väl definierad sak." Johan Commelin vid Utrechts universitet tillägger: "Vi vill förstå varför [IUT], och vi har väntat på det i mer än 10 år. Lean skulle kunna hjälpa oss att förstå de svaren."
Ändå är uppgiften enorm och kräver team av specialister och potentiellt år av arbete. Även framgång kanske inte avslutar debatter om tolkning, som Mochizuki erkänner att Lean inte erbjuder någon "magisk kur" för sociala problem. Buzzard förblir optimistisk: "Man kan inte argumentera med mjukvaran."