Od génia se zápisníkem k matematice jako softwarovému projektu
Po staletí se matematici spoléhali výhradně na pero, papír a bystrost svých kolegů. Dnes tiše vstupuje do hry nový pomocník — software jménem Lean, který pracuje v zákulisí.
Stále více předních matematiků nechává své nejsložitější důkazy kontrolovat speciálním softwarem řádek po řádku. Programy jako Lean prohledávají tisíce stran plných vzorců, hledají chyby a vydávají jednoznačný verdikt: je důkaz skutečně správný, nebo se někde skrývá trhlina?
Kdy se začalo měnit tradiční pojetí matematiky
V klasické představě sedí matematik sám v místnosti obklopený zápisníky. Po měsících nebo letech vznikne důkaz, který trpělivě pročítají kolegové. Tento přístup fungoval tři tisíce let — od Archiméda hluboko do dvacátého století.
Jenže tento obraz se dnes viditelně mění. Jedním z klíčových momentů byl přínos německého špičkového matematika Petera Scholzeho, nositele prestižní Fieldsovy medaile. Publikoval vysoce technickou teorii o takzvaných „kondenzovaných prostorech" — tématu, jemuž ve světě skutečně rozumí jen hrstka lidí.
Scholze si nebyl vůbec jistý. Jeho důkaz čítal stovky stran plných jemných kroků, kde bylo snadné se ztratit. Místo toho, aby znovu obcházel kolegy s prosbou o přečtení, rozhodl se postupovat radikálně jinak.
Lean jako digitální spolučtenář
V roce 2020 Scholze spustil projekt nazvaný Liquid Tensor Experiment — otevřenou výzvu pro každého, kdo uměl pracovat s Leanem, takzvaným proof assistantem. Jde o software, který převádí matematické úvahy do formálního kódu a podrobuje každý krok přísné logické zkoušce.
Mezinárodní skupina výzkumníků se do projektu ponořila. Překládali Scholzeho složitou argumentaci do kódu kousek po kousku, až vzniklo přibližně 180 000 řádků. Lean pak neúnavně procházel celým dílem a ověřoval, zda každý krok vychází z předchozích kroků a z dohodnutých definic použitých pojmů.
Zatímco lidská kontrola vždy obsahuje jistou míru důvěry, Lean zazvoní na poplach teprve tehdy, když je vše formálně v pořádku.
Po půl roce práce přišla vytoužená odpověď: důkaz obstál bez logických mezer. Pro Scholzeho to znamenalo jistotu, kterou mu žádný lidský recenzent nikdy nemohl poskytnout. Pro matematickou komunitu to bylo symbolické rozloučení se starou tradicí — s oním „věřte nám, dlouho jsme to kontrolovali".
Projekty, které byly dříve nepředstavitelné, jsou nyní proveditelné
Proof assistants neslouží jen k uklidnění jednotlivých hvězd. Najednou zpřístupňují projekty, které byly dříve prakticky neproveditelné.
Známým příkladem je práce Maryny Viazovské, jež vyřešila staletý problém o nejefektivnějším uspořádání koulí v osmi dimenzích. Její důkaz je proslulý svou elegancí, zároveň však obsahuje mimořádně hutné matematické pasáže. Úplná ruční kontrola by vyžadovala roky práce velké skupiny specialistů.
Mezinárodní tým se rozhodl formalizovat důkaz v Leanu. Měsíce převáděli vzorec za vzorcem do formálních výroků, jimž software dokázal porozumět. Teprve až každá část existovala jako kód, mohl Lean projít celou stavbu.
- Každý krok musel striktně vycházet z kroků předchozích.
- Žádný předpoklad nesměl nepozorovaně proniknout dovnitř.
- Každá použitá definice musela být v kódu přesně zachycena.
V roce 2024 se plná Lean verze Viazovského důkazu objevila online. Poprvé tak existovalo formální potvrzení, které by lidé sami jen stěží dokázali dodat. Projekt ukázal, že ani krajně složité výsledky nemusejí nadále zůstávat v šedé zóně nejistoty.
Mathlib jako rostoucí sada nástrojů
Důležitým důvodem, proč taková díla dnes vůbec vznikají, je obrovský růst Mathlibу — centrální knihovny Leanu. Ta v současnosti obsahuje přes 1,2 milionu řádků kódu: definice, věty a dříve formalizované důkazy.
Kdo chce do Leanu vložit nový důkaz, nemusí začínat od nuly. Mnohé základní pojmy a standardní výsledky jsou již k dispozici. To nejen šetří práci, ale také zabraňuje tomu, aby každý znovu vynalézal kolo.
Každá formalizovaná věta se stává stavebním kamenem, na němž mohou druzí přímo stavět.
Knihovna roste jako open source matematika: desítky výzkumníků denně přidávají malé i velké kousky. Společně posouvají hranici toho, co je ověřitelné.
Software, který odhaluje chyby v oceněných důkazech
Proof assistants nedávají jen zelené fajfky. Dokáží být i nepříjemně upřímní. V roce 2021 byl v Leanu formalizován důležitý, oceněný výsledek. V průběhu procesu software odmítl pokračovat — jeden mezikrok si protiřečil s vlastními výchozími předpoklady důkazu.
Zúčastnění matematici museli svou argumentaci přepracovat. Tento detail nepozoroval žádný lidský recenzent, přestože práci pečlivě přečetlo několik expertů. Chyba výsledek neznehodnotila, jasně však ukázala, jak snadno může jemná přehlédnutí proklouznout hodnoticím sítem.
Takové zkušenosti způsobují mentální posun. Kde dříve publikovaný důkaz prakticky znamenal „schváleno až do odvolání", vzniká nyní nová kategorie: výsledky, které jsou prokazatelně plně formalizovány a prošly softwarovou kontrolou.
Z niche nástroje na běžnou pomůcku
Dlouho byly proof assistenty spíše hračkami pro logiky a informatiky. Křivka učení byla strmá, rozhraní neohrabané a práh pro klasicky vzdělané matematiky vysoký. Jenže tento obraz se rychle mění.
Nové verze Leanu a podobných programů získávají uživatelsky přívětivé prostředí, v němž pomáhají AI modely. Matematici tak mohou například:
- vložit ručně psaný důkaz a automaticky obdržet návrhy formálního překladu;
- nechat doplnit, která lemmata (pomocné věty) ještě chybějí, aby byl krok uzavřený;
- okamžitě vidět, kde v argumentaci logika vázne.
Mnoho doktorandů se dnes s těmito nástroji učí pracovat již během studia. Tento přístup pak přenášejí do výzkumných projektů, čímž se přijetí nové metodiky urychluje.
Co přesně tyto systémy dělají?
Proof assistenty jako Lean, Coq nebo Isabelle fungují jinak než spektakulární AI systémy generující texty nebo obrázky. Jsou naopak kompromisně přísné.
Celý proces probíhá zhruba ve třech krocích:
| Krok | Co se děje? |
|---|---|
| 1. Formalizace | Matematik přepíše důkaz do rigidního, programovacímu jazyku podobného zápisu bez jakékoli dvojznačnosti. |
| 2. Rozložení | Důkaz se rozdělí na velmi malé, ověřitelné kroky a pomocné věty. |
| 3. Kontrola | Software ověří, zda každý krok logicky plyne z kroků předchozích a ze zaznamenaných definic. |
Zatímco lidé uvažují v širších celcích a detaily přeskakují, software vynucuje radikální přesnost. Stojí to čas, ale výsledná jistota je nevídaně vysoká.
Napětí mezi kreativitou a tvrdou kontrolou
Mezi matematiky probíhá živá diskuze: jak velký důraz klást na formální ověřování a kolik prostoru ponechat kreativním skokům? Elegantní, intuitivní argumentace napsaná na tabuli může někdy na pár řádcích objasnit celou podstatu, zatímco formální verze téhož zabere desítky stran kódu.
Mnoho výzkumníků proto vnímá nastupující dělbu práce. Intuici využívají k vymýšlení nových nápadů, rozpracování hrubých skic a hledání spojitostí mezi zdánlivě nesouvisejícími oblastmi. Software přichází na řadu teprve tehdy, když výsledek skutečně hodně váží — například proto, že řeší známou otevřenou otázku — a je potřeba ověřit, zda jsou všechny detaily logicky neprůstřelné.
V praxi tak vzniká hybridní způsob práce:
- lidé tvoří domněnky, náčrty a kreativní skoky;
- software pomáhá čistit, strukturovat a kontrolovat definitivní verzi;
- týmy roztroušené po celém světě mohou současně pracovat na různých částech téhož důkazu.
Co to znamená pro budoucnost matematiky?
Pokud současný trend pokračuje, počet formálně ověřených teorémů rychle poroste. Vznikne tak jakési „tvrdé jádro" výsledků, na nichž budou příští generace moci přímo stavět — aniž by se musely ptát, zda se v nich neskrývá chyba.
To bude mít důsledky i pro vzdělávání. Studenti budou moci trénovat v prostředí, kde software okamžitě ukáže, kde jejich argumentace selhává. Učitelé získají lepší přehled o tom, který krok důkazu studentům opakovaně dělá potíže. A mladí výzkumníci se brzy naučí, že jasná formulace ve formálním jazyce není vedlejší záležitost, ale mocný nástroj.
Pro nezasvěcené to možná zní chladně — jako by z matematiky mizela romantika. Mnoho matematiků to ale vidí jinak. Přenesením těžkopádné kontrolní práce na počítač vzniká více prostoru pro kreativní skoky, divoké nápady a nečekané souvislosti. Velká věta sice může projít Leanem, první jiskra ale stále vzniká v hlavě člověka s tužkou v ruce.
