Již více než deset let se matematická komunita zabývá vášnivou debatou o pravosti jednoho rozsáhlého a vysoce kontroverzního důkazu. Dnes se do popředí dostává nový technologický obor, počítačová formalizace, který nabízí potenciální způsob, jak tuto debatu konečně vyřešit.
Konflikt ohledně hypotézy ABC
V centru konfliktu je hypotéza ABC, základní problém týkající se vztahu mezi sčítáním a násobením prvočísel. V roce 2012 Shinichi Mochizuki z Kjótské univerzity zveřejnil 500stránkový důkaz, který měl za cíl vyřešit tuto dlouhotrvající záhadu.
Jeho metoda – vysoce komplexní teoretický rámec nazvaný Interuniversal Teichmüller Theory (IUT) – však byla tak bezprecedentní, že rozdělila globální matematickou komunitu. Zatímco Mochizuki a jeho příznivci trvají na tom, že důkaz je správný, mnoho významných matematiků, včetně Petera Scholze a Jakoba Stixe, tvrdí, že logika obsahuje fatální chybu.
Tato slepá ulička vytvořila pro moderní vědu vzácný stav „patové situace“: jedna strana vidí dílo jako průlomovou pravdu, zatímco druhá vidí nesrozumitelné nebo chybné uvažování.
Vzestup formalizace
Aby se výzkumníci dostali z tohoto začarovaného kruhu, obracejí se na Lean, specializovaný programovací jazyk určený pro „formalizaci“. V tomto procesu jsou matematické důkazy převedeny do kódu, který může počítač ověřit s naprostou logickou jistotou. Tím se odstraňuje „lidský faktor“ – možnost nedorozumění, společenský tlak nebo zaujatost při hodnocení – a nahrazuje se binární pravdou.
V současné době se dva různé projekty pokoušejí použít tuto technologii k ukončení tohoto problému:
1. Projekt LANA (Search for Truth)
Projekt Lean and Anabelian geometry (LANA) vedený Fumiharu Kato ze ZEN Math Center si klade za cíl ověřit důkaz jednou provždy. Tato skupina zahrnuje odborníky jak na specifické teorie Mochizuki, tak na programovací jazyk Lean.
I přes dosažený pokrok se projekt potýkal s velkou překážkou. Identifikovali specifický problém s teorií IUT, která odráží chybu objevenou Scholzem a Stixem v roce 2018. Po osmnácti měsících intenzivního studia se týmu stále nedaří tento logický uzel rozmotat.
2. Mochizuki Project (Search for Clarity)
Mochizuki a jeho kolegové zvolili jiný přístup a začali formalizovat svou práci v jazyce Lean. Jejich cílem však není „prokázat“ vlastní správnost (protože ji považují již za zavedenou), ale použít kód jako nástroj pro přesnou komunikaci.
Mochizuki tvrdí, že Lean vytvoří „přesný záznam“ své logické struktury, čímž se stane imunní vůči nesprávným interpretacím, které po léta živily kontroverze. Přestože jeho tým již vytvořil prvních 70 řádků kódu, odborníci podotýkají, že jde pouze o úplný začátek kolosálního díla.
Proč je to důležité?
Řešení hypotézy ABC není pouze záležitostí jedné rovnice; to je zlom v samotné praxi matematiky.
- Verification Crisis: Pokud počítač objeví chybu, ukončí to desetiletí akademických třenic.
- Nová metodika: Pokud důkaz obstojí, ukáže se, že „formalizace“ je životaschopný způsob, jak se vypořádat s matematickými myšlenkami, jejichž složitost přesahuje lidské kognitivní limity.
- Bridge for Communication: Dialog mezi projektem LANA a Mochizukiho skupinou ukazuje, že technologie může konečně poskytnout společný jazyk pro matematiky, kteří jinak nejsou schopni spolu efektivně komunikovat.
Závěr
Přes obrovské technické potíže představuje přechod k počítačově ověřitelné matematice první skutečný pohyb v kontroverzi ABC hypotézy po mnoha letech. Ať už kód potvrdí Mochizukiho práci nebo ji opraví, výsledek zásadně změní způsob, jakým je stanovena a sdělována matematická pravda.
