Od ponad dziesięciu lat społeczność matematyczna toczy gorącą debatę na temat autentyczności jednego zakrojonego na dużą skalę i wysoce kontrowersyjnego dowodu. Dziś na pierwszy plan wysuwa się nowa dziedzina technologiczna, formalizacja komputerowa, oferująca potencjalny sposób na ostateczne rozwiązanie tej debaty.
Konflikt wokół hipotezy ABC
W centrum konfliktu znajduje się hipoteza ABC, zasadniczy problem dotyczący związku pomiędzy dodawaniem i mnożeniem liczb pierwszych. W 2012 roku Shinichi Mochizuki z Uniwersytetu w Kioto opublikował 500-stronicowy dowód mający na celu rozwiązanie tej wieloletniej tajemnicy.
Jednakże jego metoda – bardzo złożone ramy teoretyczne zwane Międzyuniwersalną teorią Teichmüllera (IUT) – była tak bezprecedensowa, że podzieliła światową społeczność matematyczną. Choć Mochizuki i jego zwolennicy upierają się, że dowód jest poprawny, wielu wybitnych matematyków, w tym Peter Scholze i Jakob Stix, twierdzi, że logika ta zawiera fatalny błąd.
Ten impas spowodował rzadki stan „impasu” we współczesnej nauce: jedna strona postrzega tę pracę jako przełomową prawdę, podczas gdy druga widzi niezrozumiałe lub błędne rozumowanie.
Powstanie formalizacji
Aby wyrwać się z tego błędnego koła, badacze zwracają się ku Lean, specjalistycznemu językowi programowania zaprojektowanemu z myślą o „formalizacji”. W tym procesie dowody matematyczne są tłumaczone na kod, który komputer może zweryfikować z absolutną logiczną pewnością. Eliminuje to „czynnik ludzki” – możliwość nieporozumień, presji społecznej lub stronniczości podczas recenzowania – i zastępuje go prawdą binarną.
Obecnie dwa różne projekty próbują wykorzystać tę technologię, aby położyć kres temu problemowi:
1. Projekt LANA (Poszukiwanie Prawdy)
Prowadzony przez Fumiharu Kato z ZEN Math Center projekt Lean and Anabelian Geometry (LANA) ma na celu raz na zawsze zweryfikować dowód. W tej grupie znajdują się eksperci zarówno w zakresie specyficznych teorii Mochizuki, jak i języka programowania Lean.
Pomimo poczynionych postępów projekt napotkał poważną przeszkodę. Zidentyfikowali konkretny problem z teorią IUT, który odzwierciedla wadę odkrytą przez Scholze i Stixa w 2018 r. Po osiemnastu miesiącach intensywnych badań zespół nadal nie może rozwikłać tego logicznego węzła.
2. Projekt Mochizuki (Poszukiwanie przejrzystości)
Przyjmując inne podejście, Mochizuki i jego współpracownicy również zaczęli formalizować swoją pracę w języku Lean. Ich celem nie jest jednak „udowodnienie” własnej słuszności (bo uważają ją za już ustaloną), ale wykorzystanie kodu jako narzędzia trafnej komunikacji.
Mochizuki twierdzi, że Lean stworzy „dokładny zapis” swojej logicznej struktury, uodporniając go na błędne interpretacje, które od lat budzą kontrowersje. Choć jego zespół stworzył już pierwsze 70 linii kodu, eksperci zauważają, że to dopiero początek kolosalnej pracy.
Dlaczego to jest ważne?
Rozwiązanie hipotezy ABC nie jest po prostu kwestią jednego równania; jest to punkt zwrotny w samej praktyce matematyki.
- Kryzys weryfikacji: Jeśli komputer wykryje błąd, zakończy się dekada tarć akademickich.
- Nowa metodologia: Jeśli dowód się sprawdzi, udowodni, że „formalizacja” jest realną metodą radzenia sobie z ideami matematycznymi, których złożoność przekracza ludzkie granice poznawcze.
- Pomost komunikacji: Dialog pomiędzy projektem LANA a grupą Mochizuki pokazuje, że technologia może wreszcie zapewnić wspólny język matematykom, którzy w innym przypadku nie byliby w stanie skutecznie się ze sobą porozumiewać.
Wniosek
Pomimo ogromnych trudności technicznych przejście do matematyki weryfikowalnej komputerowo stanowi pierwszy od wielu lat prawdziwy ruch w kontrowersji wokół hipotezy ABC. Niezależnie od tego, czy kod potwierdzi pracę Mochizukiego, czy też ją poprawi, wynik zasadniczo zmieni sposób ustalania i przekazywania prawdy matematycznej.
