Tam, kde matematici dříve spoléhali na červené tužky a stohy papíru, si dnes k jejich stolu přisedá tichý, neúprosný software.
Nové programy prochází matematické důkazy řádek po řádku, aniž by se unavily nebo ztratily nit. Přední světové matematické kapacity nechávají své nejsložitější věty prověřovat systémy jako Lean, který odhaluje chyby tam, kde by je žádný člověk nikdy nenašel.
Od osamělého myslitele k matematickému týmu s počítačovými pomocníky
Matematika měla po staletí něco osamělého. Vědec se stáhl do ústraní, pracoval roky na důkazu a pak ho poslal malé skupině kolegů. Ti vše pečlivě četli, někdy celé měsíce. Nakonec přišlo tiché potřesení rukou: všichni předpokládají, že to sedí.
V praxi se ukázalo, že tento přístup je zranitelný. Důkazy moderních vět snadno pokrývají stovky stránek. Zapomenutá podmínka, příliš rychlá úvaha, chybné přepsání — drobné přehmaty mohou mít zásadní následky. Přesto snadno proklouznou, protože skoro nikdo není schopen projít takové dílo do posledního detailu.
Německý matematický talent Peter Scholze pocítil toto napětí na vlastní kůži. Získal prestižní Fieldsovu medaili, patří k absolutní špičce oboru, a přesto ho hlodaly pochybnosti ohledně obrovského důkazu týkajícího se takzvaných „kondenzovaných prostorů". Pouhá hrstka odborníků vůbec chápala, o čem mluví. Natož aby někdo dokázal celý důkaz plně překontrolovat.
Veřejný experiment s počítačem jako rozhodčím
Místo hledání dalších lidských čtenářů zvolil Scholze jinou cestu. V roce 2020 spustil Liquid Tensor Experiment — otevřenou výzvu pro matematiky a programátory, aby jeho práci přeložili do systému Lean, takzvaného proof assistantu.
Proof assistant není kalkulačka, ale přísný účetní logiky. Uživatel napíše důkaz ve formálním jazyce. Software zkontroluje každý krok: vyplývá toto pravidlo skutečně z předchozího, podle dohodnutých axiomů a definic? Pokud ne, systém odmítne pokračovat. Žádné výjimky, žádná reputace, jen čistá konzistentnost.
Po celém světě se výzkumníci pustili do Scholzeovy výzvy. Místo jednoho izolovaného génia se zápisníkem vzniklo online staveniště: desítky lidí pracovaly na drobných kouscích téhož důkazu. Lean a centrální knihovna mathlib přitom hlídaly celkovou soudržnost.
Po šesti měsících bylo hotovo 180 000 řádků Lean kódu — dostatek pro formální potvrzení, že Scholzeova věta obstojí bez logických mezer.
Pro Scholzeho to představovalo jiný druh jistoty než tradiční peer review. Nikoli „nikdo zatím nenašel chybu", ale „každý logický krok je explicitně zaznamenaný a přijatý softwarem". Pro mnoho matematiků se tento okamžik stal přelomovým bodem.
Zdánlivě nesplnitelné megaprojekty se najednou stávají realizovatelnými
Scholzeův příběh není ojedinělý. V roce 2016 vyřešila Maryna Viazovska staletý rébus: jak co nejefektivněji uspořádat koule v osmi dimenzích? Její řešení bylo světově oslavováno a v roce 2022 jí vyneslo také Fieldsovu medaili.
Přesto s tím byl spojen praktický problém. Její důkaz je zapsán neobyčejně kompaktně, ale je konceptuálně a technicky natolik náročný, že důkladná kontrola lidmi trvá roky. Reálná šance, že nějaký detail zůstane nepovšimnuto chybný, rozhodně existuje.
Mezinárodní skupina výzkumníků se proto rozhodla formalizovat její práci v Lean, stejně jako u Scholzeho. Měsíce pracovali na digitální verzi jejího postupu. V roce 2024 byl publikován kompletní kód, volně přístupný pro každého. Lean vším prošel a potvrdil, že struktura důkazu je bezchybná.
- Obrovské důkazy se rozkouskují na malé, zvládnutelné lemmata.
- Týmy mohou paralelně pracovat na různých částech.
- Software hlídá, aby všechny části do sebe logicky zapadly.
- Výsledný kód slouží jako trvalý, ověřitelný archiv.
Dříve některé velké domněnky zůstávaly neprověřeny prostě proto, že se nikdo neodvážil proplétat tisíce řádků úvah. Dnes roste přesvědčení, že výmluva „příliš velké na kontrolu" pomalu mizí. Nástroje jako Lean, Coq a Isabelle z takových projektů dělají zvládnutelné úkoly — za předpokladu, že se zapojí dostatek lidí.
Mathlib: něco jako GitHub pro matematické jistoty
Klíčovou roli hraje mathlib, centrální knihovna systému Lean. Ta nyní obsahuje více než 1,2 milionu řádků definic, tvrzení a důkazů — od základní aritmetiky a teorie grup až po pokročilou analýzu.
Kdo chce formalizovat nový důkaz, nemusí vše budovat od nuly. Opírá se o dříve zaznamenané výsledky, podobně jako se programátoři spoléhají na existující softwarové balíčky. To každý nový projekt urychluje a zvyšuje atraktivitu proof assistantů.
Pokaždé, když je přidána nová věta, roste hodnota celého ekosystému. Každý další výzkumník může začít o krok dále.
Software, který odhaluje chyby v oceňovaných důkazech
Role těchto systémů se neomezuje jen na potvrzování správnosti. Ukazují také, kde lidské úvahy ve skutečnosti nesedí. V roce 2021 formalizoval tým dříve oceněnou větu v Lean. V polovině procesu software odmítl pokračovat — někde chyběl zásadní krok.
Autoři se ponořili zpět do vlastní práce a zjistili, že počítač měl pravdu. Původní článek musel být opraven. Žádný recenzent chybu neodhalil, přestože logika vykazovala závažnou mezeru.
Takové případy udávají tón. Zatímco lidský čtenář někdy usoudí „tato část bude určitě v pořádku", software nezná shovívavost. Program přijme krok pouze tehdy, pokud ho dokáže doslova odvodit z předchozích pravidel a předpokladů. Jinak se vše zastaví.
| Lidská kontrola | Kontrola proof assistantem |
|---|---|
| Pracuje s intuicí a zkušeností | Pracuje se striktně formálními pravidly |
| Může části přeskočit nebo shrnout | Prochází každý krok bez výjimky |
| Unaví se, ztrácí koncentraci | Zůstává konzistentní i po milionech řádků |
| Ovlivnitelná reputací nebo statusem | Neutrální: rozhoduje jen logika |
Díky AI se vstupní bariéra snižuje
Dlouhou dobu byly tyto nástroje především hračkou pro informatiky. Křivka učení byla strmá, jazyk přísný a málo odpouštějící. Matematici bez programátorských zkušeností rychle odpadávali.
Tento obraz se mění. Nová rozhraní, často s pomocí AI modelů, překládají neformální matematiku do formálního Lean kódu. Výzkumník může nastínit důkaz tak, jak je zvyklý, a asistent nabídne návrhy odpovídajících příkazů v Lean.
Univerzity zakládají pracovní skupiny, kde doktorandi rovnou budují své důkazy v takovém systému. Tím se učí současně moderní matematiku i disciplínu přesně formulovat každý krok. Software funguje skoro jako přísný vedoucí, který nepřehlíží žádnou nepřesnost.
Co to znamená pro budoucnost matematiky?
Nástup proof assistantů se dotýká citlivé otázky: kdo nebo co vlastně větu „chápe"? Člověk, který přijde s nápadem, nebo stroj, který dokáže, že každá část logicky sedí? V praxi vzniká hybridní model.
Intuice, kreativita a hledání překvapivých spojení zůstávají lidskou doménou; počítač hlídá, aby zpracování nikde nevybočilo z logické dráhy.
V oblastech, kde matematika přímo vstupuje do techniky — jako kryptografie, letecký design nebo výroba čipů — získává formální ověřování mimořádný význam. Drobná chyba v důkazu bezpečnostního protokolu může učinit zranitelným zařízení v hodnotě miliard. Firmy i výzkumné instituce proto stále častěji hledají nástroje, které dokáží matematické jistoty zaručit.
Kdo matematiku studuje nebo vyučuje, může tento vývoj využít velmi konkrétně. Formalizování menších tvrzení z analýzy nebo algebry v proof assistantu nutí studenty k přesnému vyjadřování a odkrývá implicitní předpoklady. Učitelé tak vidí, kde úvahy skutečně drhnou.
Pro nezasvěcené to možná vypadá, jako by matematici vyměňovali své tajemno za nudný kód. Ve skutečnosti se děje něco jiného: intuitivní skoky a kreativní nápady zůstávají, ale již nezanikají v neprostupných rukopisech. Dostávají formu, kterou může každá příští generace krok za krokem sledovat, ověřovat a rozšiřovat — s počítačem jako neúnavným spolučtenářem.
