Důkaz kontroluje počítač. Musíme mu jen věřit?
Čtyři pastelky stačí. Proč to ale není totéž jako vyzkoušet hodně map — a co nám strojově ověřený důkaz řekne o správnosti, významu a porozumění.
V článku
Představme si stůl, mapu a čtyři pastelky. Sousední oblasti nesmějí mít stejnou barvu. Chvíli to jde. Pak uprostřed zbude bílé místo, kolem kterého už svítí všechny čtyři. Sáhnete po páté.
„Tu nepotřebuješ,“ řekne někdo od notebooku. „Je to dokázané.“
„Výborně. A jak?“
Scéna je vymyšlená. Otázka nikoli. Co nám dává právo věřit důkazu, jehož všechny kroky sami neprojdeme? A když počítač potvrdí výsledek, znamená to, že mu také rozumíme?
Čtyři stačí. Jen možná musíte začít znovu
Věta o čtyřech barvách říká, že pro obarvení rovinné mapy stačí nejvýše čtyři barvy. Vezměme zde konečnou mapu se souvislými oblastmi a hranicemi z úseček. Oblasti se společným kusem hranice musejí mít různé barvy. Dotyk v jediném bodě nevadí.[5]
Není to slib, že uspěje každý postup. Pokud jste pastelky rozdávali nešťastně, můžete se zaseknout. Věta slibuje, že vhodné obarvení existuje. Ne že ocení vaši dosavadní práci.
Kenneth Appel a Wolfgang Haken přišli v roce 1976 s průlomovým důkazem, který podstatně využíval počítačovou kontrolu.[5] To ovšem neznamená, že nechali stroj obarvit spoustu map a po úspěšném víkendu prohlásili problém za vyřešený.
Ne vzorek. Všechny potřebné případy
Rozdíl je zásadní. Zkoušení vybraných map nevyloučí, že některá další bude výjimka. Důkaz musí vysvětlit, proč žádná výjimka neunikne.
Jeho kostru si můžeme zjednodušeně představit takto. Kdyby existovala mapa, na kterou čtyři barvy nestačí, existoval by také nejmenší takový protipříklad. Matematická část argumentu ukáže, že by musel obsahovat alespoň jedno uspořádání z určitého konečného seznamu.[5]
U každého uspořádání se pak ověří, že v nejmenším protipříkladu být nemůže: vhodným zjednodušením dostaneme menší mapu a její obarvení lze upravit a přenést zpět.[5] Údajný nejmenší potížista tedy nemá kam patřit.
Počítač pomáhá s rozsáhlou kontrolou případů. Obecný argument zajišťuje, že seznam stačí.[5] Úplná kontrola po prokázaném zúžení úlohy není totéž co velký vzorek. Záleží na tom zúžení. Bez něj máme jen pilného sběratele povedených obrázků.
Program doběhl. To ještě není důkaz
Námitka se nabízí: co když má kontrolní program chybu? Gonthier ve svém přehledu upozorňuje, že opakované spuštění stejného kódu se stejným vstupem chybu programátora snadno mine.[5] Vytrvalost může omylu zajistit dlouhou kariéru.
Proto je důležité odlišit výpočet od formálního ověření. V něm jsou tvrzení a důkaz zapsány přesně tak, aby systém mohl zkontrolovat odvození podle stanovených pravidel. Lze také dokázat, že použitý výpočetní postup skutečně ověřuje požadovanou vlastnost.[5]
Georges Gonthier dokončil v roce 2005 formální důkaz věty o čtyřech barvách v systému Coq.[5] Vycházel přitom z pozdějšího přepracování důkazu, ne přímo z původní práce Appela a Hakena.[5] Počítač tu nejen vydal odpověď. Kontroloval matematické zdůvodnění, včetně vazby mezi výpočty a tvrzením.[5]
Je to rozdíl mezi oznámením „vyšlo mi to“ a předložením argumentu v podobě určené ke kontrole. Takto zapsané důkazy lze uchovat a nezávisle kontrolovat.[5] Zelená kontrolka získává význam teprve tím, co stojí za ní.
Kdo kontroluje kontrolora?
Nejsilnější námitka není, že matematika patří křídě. Rozhodující část argumentu nemůžeme osobně projít. Spoléháme na stroj. Co tedy vlastně víme? Filozofka Katia Parshina rozebírá právě tuto obavu: do jistoty matematického důkazu se přidává důvěra, že počítač opravdu pracoval správně.[4]
Nestačí odpovědět, že lidé také chybují. Tím jsme oba účastníky urazili, ale kontrolu nezlepšili.
Formální ověření nabízí přesněji vymezený předmět kontroly. Parshina přitom rozlišuje důkazy, v nichž počítač zpracuje jen část, od úplné formalizace. Stejná námitka proti chybám pomocného programu proto nemá v obou případech stejnou sílu.[4] Není to však slib neomylného softwaru či hardwaru.
Zbývá také překlad otázky. Gonthier výslovně připomíná, že čtenář musí prozkoumat definice, aby zjistil, zda formální tvrzení skutečně odpovídá tomu, co slibuje jeho název.[5] Dokonale ověřená odpověď na jinou otázku je stále odpověď na jinou otázku. Jen má hezčí razítko.
Vědět, že ano. A pochopit proč
I správný důkaz může čtenáře nechat nespokojeného. Chce vidět nosný nápad, nejen vyloučené možnosti. Přehled ve Stanfordské encyklopedii popisuje, jak matematici znovu dokazují známé výsledky právě kvůli lepšímu vysvětlení. Co přesně dělá důkaz vysvětlujícím, zůstává předmětem sporu.[2]
Nebylo by ale fér rozdělit práci tak, že člověk rozumí a stroj jen odškrtává. Gonthier popisuje, že nutnost rozepsat argument přesně přinesla nové vhledy a zjednodušení.[5] Kontrola někdy pomůže objevit, čemu jsme dosud rozuměli jen velkoryse.
Náš závěr je tedy střízlivější než „věřte počítačům“. Ptejme se zvlášť: Je argument správný? Odpovídá na naši otázku? Pomáhá nám pochopit proč? Jedno ano nenahrazuje zbývající dvě.
Co by změnilo náš názor
Konkrétní chyba v kontrolním systému nebo nesoulad mezi definicemi a zamýšlenou větou by naši důvěru v daný důkaz oslabil. Sám o sobě by ale ještě nedokazoval, že věta je nepravdivá.
Naopak skutečně nezávislá kontrola téhož přesného tvrzení by důvěru posílila. Kratší, lépe vysvětlující důkaz by zase mohl zlepšit porozumění, aniž by tím starý správný důkaz přestal platit.
Nemusíme všechno osobně přepočítat. Měli bychom však vědět, co bylo kontrolováno a co nikoli. Pátou pastelku lze odložit. Otázku „a proč?“ si nechme.
Meze rešerše: výběrová esej nad Gonthierovým technickým přehledem a filozofickými rozbory, nikoli vlastní spuštění či audit důkazu v Coq. Úvodní scéna je modelová. Výklad nejmenšího protipříkladu zachycuje jen kostru argumentu, ne úplný důkaz.
Ilustrace jsou metafory vytvořené v Higgsfieldu pomocí GPT Image 2, nikoli matematické diagramy nebo dokumentární snímky.
Zdroje
- Stanford Encyclopedia of Philosophy: Mathematical ExplanationZpět k citaci 1
- Katia Parshina: Philosophical Assumptions Behind the Rejection of Computer-Based Proofs (2023)Zpět k citaci 1 Zpět k citaci 2
- Georges Gonthier: Formal Proof—The Four-Color Theorem (2008), úplná kopie CornellZpět k citaci 1 Zpět k citaci 2 Zpět k citaci 3 Zpět k citaci 4 Zpět k citaci 5 Zpět k citaci 6 Zpět k citaci 7 Zpět k citaci 8 Zpět k citaci 9 Zpět k citaci 10 Zpět k citaci 11 Zpět k citaci 12 Zpět k citaci 13