Jedna z najbardziej kontrowersyjnych debat matematycznych mogłaby zostać rozstrzygnięta przy pomocy komputera, co potencjalnie zakończyłoby gorzki spór dotyczący złożonego dowodu trwającego od ponad dekady.
Problemy zaczęły się w 2012 roku, gdy Shinichi Mochizuki z Uniwersytetu w Kioto w Japonii zaskoczył świat matematyki rozbudowanym, 500-stronicowym dowodem dla hipotezy ABC, ważnego nierozwiązanego problemu, który uderza w samo serce tego, czym są liczby. Dowód wykorzystywał bardzo skomplikowaną i niewyobrażalną strukturę wymyśloną przez Mochizuki’ego, zwaną teorią inter-universalną Teichmüllera (IUT), która wydawała się nieprzenikniona nawet dla większości ekspertów matematyków starających się ją zrozumieć.
Hipoteza ABC, która ma ponad 40 lat, obejmuje pozornie prostą równość trzech liczb całkowitych a + b = c i określa, jak liczby pierwsze tworzące te liczby muszą się do siebie odnosić. Oprócz głębokich wglądów w fundamentalną naturę interakcji dodawania i mnożenia, hipoteza ma implikacje dla innych znanych matematycznych hipotez, takich jak Wielkie Twierdzenie Fermata.
Potencjalne konsekwencje te sprawiły, że matematycy początkowo byli entuzjastyczni co do zweryfikowania dowodu, ale wczesne wysiłki załamały się, a Mochizuki ubolewał, że nie włożono więcej wysiłku w przyswojenie jego pracy. Następnie w 2018 roku dwaj znakomici niemieccy matematycy, Peter Scholze z Uniwersytetu w Bonn i Jakob Stix z Uniwersytetu Goethe we Frankfurcie, ogłosili znalezienie możliwej luki w zbroi dowodu.
Mochizuki jednak odrzucił ich argument, a brak wielkiego organu orzekającego o tym, kto ma rację, a kto nie, spowodował, że ważność teorii IUT skrystalizowała się w dwóch obozach: z jednej strony większość społeczności matematycznej, a z drugiej niewielka grupa badaczy luźno związanych z Mochizuki’m i Instytutem Badań nad Naukami Matematycznymi w Kioto, gdzie jest profesorem.
Teraz Mochizuki zaproponował możliwe rozwiązanie impasu. Zaproponował przetłumaczenie dowodu z jego obecnej postaci, w notacji matematycznej przeznaczonej dla ludzi, na język programowania o nazwie Lean, który mógłby zostać automatycznie sprawdzony i zweryfikowany przez komputer.
Ten proces, nazywany formalizacją, jest ciągłym obszarem badań, który może całkowicie zmienić sposób, w jaki jest wykonywana matematyka. Sugestie formalizacji dowodu Mochizukiego były już wcześniej wysuwane, ale to pierwszy raz, kiedy on wyraził chęć kontynuacji projektu.
Mochizuki nie odpowiedział na prośbę o skomentowanie tego artykułu, ale w niedawno opublikowanym raporcie argumentował, że Lean nadaje się doskonale do rozwiązania konfliktów między matematykami, które uniemożliwiły powszechne przyjęcie jego dowodu: „[Lean] jest najlepszą i być może jedyną technologią… do osiągnięcia rzeczywistego postępu w zakresie fundamentalnego celu uwolnienia prawdy matematycznej od jarzma dynamiki społecznej i politycznej,” pisze Mochizuki.
Według Mochizukiego został przekonany o zaletach formalizacji po uczestnictwie w niedawnej konferencji na temat Lean w Tokio w lipcu, zwłaszcza po zobaczeniu jego zdolności do obsługi struktur matematycznych, które są niezbędne dla jego teorii IUT.
To potencjalnie obiecujący kierunek pomocy w pokonaniu impasu – mówi Kevin Buzzard z Imperial College London. Jeśli coś jest zapisane w Lean, to nie jest to szaleństwo, prawda? Wiele rzeczy w pracach jest napisane w bardzo dziwnym języku, ale jeśli można to zapisać w Lean, to znaczy, że ten dziwny język stał się w pełni zdefiniowaną rzeczą – mówi.
„Chcemy zrozumieć dlaczego [IUT], i czekamy na to od ponad 10 lat,” mówi Johan Commelin z Uniwersytetu w Utrechcie w Holandii. „Lean byłby w stanie nam pomóc zrozumieć te odpowiedzi.”
Jednak zarówno Buzzard, jak i Commelin uważają, że formalizacja teorii IUT byłaby ogromnym przedsięwzięciem i wymagałaby przetłumaczenia wielu równań matematycznych, które obecnie istnieją tylko w formie czytelnej dla ludzi. Ten projekt dorównywałby niektórym z największych wysiłków w dziedzinie formalizacji, które często obejmują zespoły ekspertów matematyków i programistów Lean, trwające miesiące lub lata.
Obiecująca perspektywa ta może jednak nie być atrakcyjną propozycją dla niewielkiej grupy matematyków kwalifikujących się do podjęcia tego projektu. „Ludzie będą musieli podjąć ważną decyzję, czy chcą poświęcić wiele czasu na pracę nad projektem, który ostatecznie może się okazać nieudanym” – mówi Buzzard.
Ale nawet jeśli matematycy zdołają ukończyć projekt, a kod Lean nie wykaże sprzeczności w twierdzeniu Mochizukiego, to matematycy, w tym sam Mochizuki, wciąż mogą spierać się o jego znaczenie – twierdzi Commelin.
„Lean może mieć duży wpływ i położyć kres kontrowersji, ale tylko jeśli Mochizuki naprawdę przestrzega swojej nowej uchwały o formalizacji swojej pracy,” mówi. „Jeśli po czterech miesiącach się wycofa, mówiąc, 'Dobra, spróbowałem tego, ale Lean jest po prostu zbyt głupie, by zrozumieć mój dowód’, to będzie to tylko nowy rozdział w bardzo długiej serii rozdziałów, w których nadal mamy problem społeczny.”
I, mimo całościowego optymizmu, który Mochizuki przejawia wobec Lean, zgadza się również ze swoimi krytykami, że interpretacja znaczenia kodu może prowadzić do dalszych sporów, pisząc, że Lean „nie wydaje się w obecnej chwili stanowić jakiegokolwiek rodzaju „magicznego lekarstwa” na zupełne rozwiązanie kwestii społecznych i politycznych.”
Jednak Buzzard czuje nadzieję, że udana formalizacja może przynajmniej nieco ruszyć z miejsca dziesięcioletnią sagę, zwłaszcza jeśli Mochizuki odniesie sukces. „Z oprogramowaniem nie ma dyskusji” – mówi.
