Bezpřekročně chytají každou chybu v důkazech
Po tisíciletí byla norma stejná: tužka, papír a měsíce namáhavého ověřování skupinou vybraných odborníků. Dnes se na pracovních stolech výzkumných pracovníků objevují programy jako Lean, Coq či Isabelle, které převádějí důkazy do kódu a kontrolují je řádek po řádku s přesností, která překračuje lidské paměti a soustředění.
Od samotáře s notesem k týmům pracujícím v jednom úložišti
Tradiční představa matematika zobrazuje génia sklánějícího se nad sešitem, který týdny zdokonaluje jednu myšlenku. Tento přístup zrodil mistrovská díla, ale měl své slabiny: bylo snadné něco přehlédnout a ověřování obřích důkazů se mohlo táhnout celá desetiletí.
Příběh Petera Scholzeho, jednoho z nejvíce respektovaných dnešních matematiků a laureáta Fieldsovy medaile, se stal symbolem této transformace. V roce 2018 zveřejnil rozsáhlý, mimořádně abstraktní výsledek týkající se takzvaných kondenzovaných prostorů. Důkaz měl stovky stran a dotýkal se oblasti, které rozumí jen hrstka vědců na světě.
Scholze však nebyl zcela klidný. Obával se, že v hromadě argumentů se skrývá jemná chyba, kterou nenajdou žádní recenzenti. Místo hledání dalších lidí ochotných měsíce sledovat každý krok se obrátil na komunitu programátorů a matematiků pracujících s Leanem. Tak vznikl projekt nazvaný Liquid Tensor Experiment.
Úkol zněl jednoduše, přestože jeho provedení vyžadovalo obrovské úsilí: přepsat celý Scholzův důkaz do formálního jazyka Lean tak, aby program mohl automaticky ověřit logiku každého kroku. Do projektu se připojili specialisté z různých zemí, kteří si vyměňovali zprávy přes internet a souběžně pracovali na stejných souborech kódu.
Po zhruba půl roce vznikl formální zápis obsahující přibližně 180 tisíc řádků. Lean nenahlásil žádné neshody. Scholze dosáhl úrovně jistoty, kterou by mu nevydal žádný lidský recenzent.
Tento příběh ukázal, že matematika nemusí spočívat na modelu samotného génia, jehož práci chrání pouze pověst a názor několika autorit. Vzniká něco jako „otevřený matematický projekt", kde desítky osob mohou paralelně rozvíjet formální zápis jedné věty, přičemž program dohlíží na konzistenci celku.
Když se složité problémy stávají proveditelné skrze formalizaci
V dalším hlasitém případě zahrnula nástrojů formální oblasti vysoce obtížného klasického problému z geometrie. Maryna Viazovska vyřešila otázku týkající se nejhustšího uspořádání koulí v osmidimenzionálním prostoru – problém, který matematiky sužuje po staletí. Její důkaz, odměněný Fieldsovou medailí, byl hustý, technický a nesmírně náročný na podrobnou kontrolu.
Skupina badatelů se rozhodla přeložit celý tento materiál do kódu v Leanu. V praxi to znamenalo vytvoření počítačové verze každého pojmu, každé funkce a každého kroku zdůvodnění. Po dlouhých měsících práce vznikl úplný projekt zveřejněný v úložišti GitHub – něco jako „mechanické potvrzení", že Viazovské konstrukce neobsahují mezery.
Nejde o ojedinělý případ, ale o signál nového standardu. Donedávna mnoho působivých vět vzbudilo pochybnosti ne proto, že se zdály nepravdivé, nýbrž kvůli ohromující délce a komplexnosti důkazů. Malá chyba nebo chybějící předpoklad se mohly skrývat gdjinde uprostřed a jejich nalezení by si vyžádalo roky intenzivního studia.
Díky nástrojům typu:
- Lean – oblíbený asistent důkazů vyvíjený jako projekt s otevřeným zdrojovým kódem,
- Coq – systém původně vytvořený informatiky zabývajícími se ověřováním software,
- Isabelle – rozvinuté prostředí pro logiku a formální matematiku,
je možné rozdělit takovéto gigantické projekty na tisíce malých kroků a rozprostřít je mezi členy týmu. Stroj nezvyšuje samotný tvůrčí proces, ale otevírá možnost pečlivé kontroly toho, co dříve platilo za „příliš obrovské na skutečné prověření".
Rostoucí knihovna hotové matematiky
Jádrem Leanu tvoří knihovna Mathlib, v níž se již shromáždilo přes milion řádků formálních definic a vět. Je to jako obrovský matematický „operační systém". Nový uživatel nemusí začínat od nuly, protože může využívat již hotových popisů čísel, algebraických struktur, topologie či míry.
| Prvek ekosystému | Role v práci matematika |
|---|---|
| Mathlib | Rozsáhlá databáze již formalizované matematiky, na níž lze stavět další věty |
| Lean | Jazyk a engine, který vynucuje logickou správnost každého kroku důkazu |
| Úložiště Git | Prostor pro společnou práci desítek autorů na jednom projektu |
| Jazykové modely AI | Pomoc při překladu „lidských" náčrtů důkazu do formálního kódu |
Čím větší se tato databáze stává, tím rychleji lze formalizovat další výsledky. Výzkumný pracovník nemusí pokaždé definovat od základu pojmy známé více než sto let, stačí sáhnout po hotových modulech.
Stroj odhaluje chyby, kterých si recenzenti nevšimli
Asistenti důkazů fungují ne jen jako „automatické pečetě potvrzující správnost". Stává se, že při přepisování známé věty do formálního jazyka se ukáže, že někde schází předpoklad anebo určitý krok nelze provést bez další argumentace.
V jednom z popsaných případů skupina matematiků rozhodla formalizovat větu, za kterou autoři obdrželi prestižní cenu. Důkaz prošel recenzí v předních vědeckých časopisech, takže se zdál vzorně solidní. Když se jej však překládalo řádek po řádku do zápisu v Leanu, program se zastavil u konkrétního místa – v řetězci vyvozování chybělo správné článek.
Program si „neusmyslel", co měli autoři na mysli. Vynutil dopsání chybějící části nebo změnu argumentace tak, aby ji bylo možné provést zcela formálně.
To ukazuje, jak zásadně se liší lidské čtení od činnosti formálního systému. Recenzent, i velmi pozorný, často vyplňuje mezery intuicí: „zde autoři určitě mysleli na to a to, je to zřejmé". Stroj taková předpoklady bez důkazu nepřijímá. Z pohledu přísnosti je to obrovský přínos – zmenšuje se riziko, že do literatury proniknou práce s jemnou, leč zásadní chybou.
Asistent důkazů jako nástroj vzdělávání
Před několika lety práce s Leanem či Coqem vyžadovala téměř plnohodnotné dovednosti v programování. Dnes se situace mění. Vyvíjejí se interaktivní prostředí, zásuvné moduly populárních editorů a doplňky založené na AI, které pomáhají překládat tradiční uvažování do formálního jazyka.
Univerzity čím dál více pořádají kurzy, kde se studenti již na úrovni magisterského studia seznamují se základy formalizace. Systém jim napovídá další kroky, vyznačuje neshody, navrhuje použití existujících lemmat z knihovny. Pro začátečníky to je způsob, jak na vlastní kůži vidět, kde v jejich argumentech schází přesnost.
Co se mění v samotné matematice
Součinnost lidí s formálními systémy vytváří několik zřetelných trendů. Především roste význam velkých, týmových projektů, které připomínají spíše vývoj software než tradiční „osamělý" výzkum. Druhak se čím dál jasněji odděluje role tvůrce myšlenky a role „formálního inženýra", který ji zvládne popsat v kódu.
Někteří matematici dokonce začínají svá zdůvodnění navrhovat s ohledem na pozdější formalizaci. Snaží se vyhýbat příliš zamlženým zkratkám typu „zřejmě z definice", protože vědí, že později program bude vyžadovat daleko více detailů. Postupem času by to mohlo ovlivnit způsob psaní vědeckých publikací: místo velmi stručné formy se objeví texty okamžitě bližší tomu, co se dá vhodit do Leanu.
Takový přístup nese také praktické důsledky mimo čistou teorii. Kryptografické algoritmy, komunikační protokoly či části kódu řídící kritickou infrastrukturu se již dnes ověřují pomocí nástrojů příbuzných matematickým systémům dokazování. Čím více matematika přechází do formálního jazyka, tím snadněji se stejné metody přenášejí do inženýrství.
Proč stát za vývojem této niche, ale vlivné oblasti
Na první pohled se formalizace důkazů zdá velmi vzdálená každodennosti. Málo koga zajímá, jak vypadá zápis slavné věty jako tisíce řádků kódu. V pozadí se však vede spor o tom, čím se vlastně matematická vědomost stává v digitální éře.
Pokud nejdůležitější věty začneme brát jako formální objekty, které musí existovat ve veřejném úložišti a procházet automatickým ověřením, změní se i způsob sdílení zjištění, přiznávání uznání či vedení vědeckých sporů. Místo diskuse „mohli si recenzenti něco všimnout", bude spíš otázka „byl projekt formalizace dokončen a prošel všemi testy".
V delší perspektivě se mohou nástrojů jako Lean stát pro matematiku tím, čím je kompilátor pro programátora: nejen mechanismem kontrolujícím správnost, ale také neodmyslitelnou součástí samotného tvůrčího procesu. A to znamená, že budoucí, nejambicióznější věty budou pravděpodobně vznikat jako duo: člověk vymýšlí, stroj ověřuje, krok za krokem, bez slití úlevy.
