Ett försök att verifiera ett kontroversiellt bevis för ABC-förmodan med hjälp av mjukvara har inte gjort några framsteg. En delrapport från projektet Lean and Anabelian Geometry visar att matematiker fortfarande är oense om huruvida den underliggande teorin är giltig.
År 2012 presenterade Shinichi Mochizuki vid Kyoto universitet ett 500 sidor långt bevis för ABC-förmodan. Beviset bygger på hans Inter-universal Teichmüller-teori, som få matematiker har lyckats verifiera.
Ett projekt känt som LANA har försökt formalisera beviset i programmeringsspråket Lean. I den senaste delrapporten framgår det att medlemmarna har fört livliga diskussioner men inte lyckats nå konsensus om huruvida teorin håller.
Rapporten belyser de kvarstående problem som först lyftes fram 2018 av Peter Scholze och Jakob Stix. Abhishek Saha vid Queen Mary University of London menar att resultatet stämmer överens med de flesta matematikers uppfattning om att det finns en allvarlig lucka i teorin.
Ivan Fesenko vid Westlake University vidhåller att kritiken är felriktad och att ett formaliserat bevis förr eller senare kommer att presenteras.