Kontroverzní matematický argument – ten, který rozděluje pole na více než deset let – může nakonec vyřešit nepravděpodobný soudce: počítačový program. Srdce sporu se točí kolem pokusu Shiničiho Mochizukiho z roku 2012 vyřešit domněnku ABC, dlouhodobý problém hluboce zakořeněný v základní povaze čísel.
Hypotéza ABC se soustředí na extrémně jednoduchou rovnici zahrnující tři celá čísla: a + b = c. Zahrnuje specifická pravidla upravující, jak by prvočísla, která tvoří tato celá čísla, měla být ve vzájemném vztahu. Řešení tohoto zdánlivě elementárního problému by mohlo odemknout hluboký vhled do oblasti matematiky a potenciálně ovlivnit další slavné domněnky, jako je poslední Fermatova věta.
Mochizuki, profesor na Kjótské univerzitě v Japonsku, představil svůj argument v rámci své vlastní komplexní konstrukce nazvané Inter-Universal Teichmüller Theory (IUT). Příliš technická a pro většinu matematiků nepochopitelná povaha teorie IUT ji však učinila z velké části nečitelnou pro ty, kdo se pokusili otestovat jeho práci. Počáteční nadšení se změnilo ve zklamání, protože odborníci bojovali s jeho složitými nuancemi.
Olej do ohně přilili v roce 2018 dva prominentní němečtí matematici, Peter Scholz a Jakob Stix, potenciální chybu v Mochizukiho důkazu. Mochizuki se postavil proti jejich argumentu a při absenci zastřešujícího orgánu pro řešení matematických sporů se pole rozvrstvilo na dva tábory: na ty, kteří z velké části přijímali konvenční pohled (podporovaný většinou matematiků), a na menší skupinu, která se hlásila k Mochizukimu a jeho institutu v Kjótu.
Mochizuki nyní navrhuje cestu vpřed prostřednictvím formalizace – transformaci svého důkazu z lidsky čitelné matematické notace do Lean, programovacího jazyka speciálně navrženého pro přísné matematické ověřování. Tento proces by potenciálně umožnil počítačům automaticky kontrolovat konzistenci jeho argumentů, což by nabídlo bezprecedentní úroveň objektivity.
Mochizuki věří, že Lean má jedinečnou pozici k překonání složitých jazykových a koncepčních bariér, které brzdily pokrok v porozumění teorii IUT. Vidí to jako nástroj k osvobození matematické pravdy od potenciálních předsudků, které jsou vlastní lidské interpretaci.
I když někteří odborníci, jako Kevin Budzard z Imperial College London, vidí tento směr jako slibný, uvědomují si také obrovskou výzvu, které čelí. Formalizace teorie IUT by vyžadovala převod obrovského množství složitých rovnic do Lean syntaxe, což je podnik srovnatelný s některými z největších formalizačních projektů, které kdy byly podniknuty. Takové snahy často zahrnují celé týmy matematiků a programátorů, jejichž dokončení trvá měsíce nebo dokonce roky.
Johan Commelin z Utrechtské univerzity v Nizozemsku, i když je opatrně optimistický, zdůrazňuje, že úspěch závisí na Mochizukiho pokračující oddanosti věci. Varuje, že pokud se projekt předčasně opustí, může jít jen o nejnovější díl dlouhotrvající ságy poznamenané nevyřešenými spory.
I když bude úspěšný, poznamenává Commelin, dokonce i při počítačovém ověření kódu mohou přetrvávat neshody ohledně interpretace. Lean může vyřešit logické rozpory, ale nemusí nutně vyřešit všechny filozofické nebo koncepční neshody kolem Mochizukiho díla.
Nakonec, i když formalizace nabízí záblesk naděje na vyřešení této věčné matematické patové situace, zůstává otevřenou otázkou, zda dokáže překonat hluboce zakořeněné složitosti a odlišné názory, které charakterizovaly debatu o prokázání domněnky ABC.
