Kontrowersyjny argument matematyczny – taki, który dzieli dziedziny od ponad dziesięciu lat – może w końcu zostać rozstrzygnięty przez nieoczekiwanego sędziego: program komputerowy. Sedno kontrowersji koncentruje się wokół podjętej w 2012 roku przez Shinichi Mochizuki próby rozwiązania hipotezy ABC, długotrwałego problemu głęboko zakorzenionego w fundamentalnej naturze liczb.
Hipoteza ABC opiera się na niezwykle prostym równaniu składającym się z trzech liczb całkowitych: a + b = c. Obejmuje określone zasady określające, w jaki sposób liczby pierwsze tworzące te liczby całkowite powinny być ze sobą powiązane. Rozwiązanie tego pozornie elementarnego problemu może odblokować głęboki wgląd w dziedzinę matematyki, potencjalnie wpływając na inne słynne hipotezy, takie jak ostatnie twierdzenie Fermata.
Mochizuki, profesor na Uniwersytecie w Kioto w Japonii, przedstawił swoją argumentację w ramach własnego złożonego konstruktu zwanego Międzyuniwersalną Teorią Teichmüllera (IUT). Jednak zbyt techniczny i niezrozumiały charakter teorii IUT dla większości matematyków sprawił, że była ona w dużej mierze nieczytelna dla tych, którzy próbowali przetestować jego pracę. Początkowy entuzjazm przerodził się w rozczarowanie, gdy eksperci zmagali się ze skomplikowanymi niuansami.
Dolewając oliwy do ognia, w 2018 roku dwóch wybitnych niemieckich matematyków, Peter Scholz i Jakob Stix, zidentyfikowało potencjalny błąd w dowodzie Mochizukiego. Mochizuki przeciwstawił się ich argumentowi i wobec braku nadrzędnego organu rozstrzygającego spory matematyczne, dziedzina ta podzieliła się na dwa obozy: tych, którzy w dużej mierze akceptowali konwencjonalny pogląd (popierany przez większość matematyków) oraz mniejszą grupę sprzymierzoną z Mochizukim i jego instytutem w Kioto.
Mochizuki proponuje teraz rozwiązanie polegające na formalizacji — przekształcenie swojego dowodu z czytelnej dla człowieka notacji matematycznej na Lean, język programowania zaprojektowany specjalnie do rygorystycznej weryfikacji matematycznej. Proces ten potencjalnie pozwoliłby komputerom automatycznie sprawdzić spójność jego argumentów, oferując niespotykany dotąd poziom obiektywizmu.
Mochizuki wierzy, że Lean ma wyjątkową pozycję do pokonania złożonych barier językowych i pojęciowych, które hamują postęp w rozumieniu teorii IUT. Postrzega ją jako narzędzie uwalniające prawdę matematyczną od potencjalnych uprzedzeń tkwiących w ludzkiej interpretacji.
Chociaż niektórzy eksperci, na przykład Kevin Budzard z Imperial College London, postrzegają ten kierunek jako obiecujący, dostrzegają także ogromne wyzwanie, jakie przed nim stoi. Sformalizowanie teorii IUT wymagałoby przetłumaczenia ogromnej masy złożonych równań na składnię Lean, co byłoby przedsięwzięciem porównywalnym z niektórymi z największych projektów formalizacyjnych, jakie kiedykolwiek podjęto. W takie wysiłki często angażują się całe zespoły matematyków i programistów, a ich ukończenie zajmuje miesiące, a nawet lata.
Johan Commelin z Uniwersytetu w Utrechcie w Holandii, mimo ostrożnego optymizmu, podkreśla, że sukces zależy od ciągłego zaangażowania Mochizukiego w sprawę. Ostrzega, że jeśli projekt zostanie porzucony przedwcześnie, może to być dopiero najnowszy odcinek długotrwałej sagi naznaczonej nierozwiązanymi sporami.
Jak zauważa Commelin, nawet jeśli kod się powiedzie, nawet po komputerowej weryfikacji kodu mogą utrzymywać się spory dotyczące interpretacji. Lean może rozwiązać logiczne sprzeczności, ale niekoniecznie rozwiązuje wszystkie filozoficzne lub koncepcyjne nieporozumienia wokół pracy Mochizuki.
Ostatecznie, chociaż formalizacja daje promyk nadziei na rozwiązanie tego odwiecznego matematycznego konfliktu, otwartym pytaniem pozostaje, czy uda jej się przezwyciężyć głęboko zakorzenione zawiłości i różne punkty widzenia, które charakteryzują debatę na temat udowodnienia hipotezy ABC.
