Tam, kde matematici dříve spoléhali na červené tužky a hromady papíru, tiše a nemilosrdně přebírá kontrolu software.
Nové programy prověřují matematické důkazy řádek po řádku, aniž by se unavily nebo ztratily nit. Přední matematici světa nechávají své nejsložitější věty kontrolovat systémy jako Lean, který odhaluje chyby, na které by žádný člověk nepřiš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. Badatel se stáhl do ústraní, roky pracoval na důkazu a pak ho odeslal malé skupině kolegů. Ti vše četli, někdy měsíce. Na závěr přišlo tiché přikývnutí: všichni předpokládali, že to sedí.
V praxi se ukázalo, že tento přístup je zranitelný. Důkazy moderních vět snadno čítají stovky stran. Přehlédnutá podmínka, příliš rychlý úsudek, chybný přepis — malá zaváhání mohou mít velké následky. Přitom snadno proklouznou, protože téměř nikdo nedokáže takové dílo zkontrolovat do posledního detailu.
Německý matematický talent Peter Scholze tuto tenzi pocítil na vlastní kůži. Přestože získal prestižní Fieldsovu medaili a patří k absolutní světové špičce, trápily ho pochybnosti ohledně obrovského důkazu týkajícího se takzvaných „kondenzovaných prostorů". Jen hrstka odborníků vůbec chápala, o čem mluví — natož aby byl někdo schopen celý důkaz pečlivě ověřit.
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 matematikům a programátorům, aby jeho práci přeložili do systému Lean, takzvaného asistenta pro ověřování důkazů.
Takový asistent není kalkulačka — je to přísný účetní logiky. Uživatel zapíše důkaz ve formálním jazyce a 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é kamarádíčkování, žádná reputace — jen čistá konzistence.
Po celém světě se výzkumníci pustili do Scholzeovy výzvy. Namísto jediného izolovaného génia s poznámkovým blokem vzniklo online staveniště: desítky lidí pracovaly na malých úsecích téhož důkazu. Lean a centrální knihovna mathlib průběžně hlídaly celkovou soudržnost.
Po šesti měsících existovalo 180 000 řádků kódu v Leanu — 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í odborné recenzování. Nikoli „nikdo dosud nenašel chybu", ale „každý logický krok je explicitně zaznamenán a software ho přijal". Pro mnoho matematiků tento okamžik znamenal zlomový bod.
Zdánlivě nesplnitelné megaprojekty se stávají uskutečnitelnými
Scholzeův příběh nestojí osaměle. V roce 2016 vyřešila Maryna Vjazovská starobylou záhadu: jak co nejefektivněji uspořádat koule v osmi dimenzích? Její řešení sklidilo celosvětový obdiv a v roce 2022 jí vyneslo také Fieldsovu medaili.
Přesto se k důkazu vázal praktický problém. Je zapsán neobyčejně kompaktně, ale konceptuálně a technicky tak náročně, že důkladná lidská kontrola by trvala roky. Riziko, že by nějaký detail zůstal nepozorovaně chybný, bylo reálné.
Mezinárodní skupina výzkumníků se proto rozhodla — stejně jako v případě Scholzeho — formalizovat její práci v systému Lean. Měsíce pracovali na digitální verzi jejího uvažování. V roce 2024 se objevil kompletní kód, volně přístupný ke kontrole. Lean celý důkaz prošel a potvrdil, že struktura je bezchybná.
- Obrovské důkazy se rozstřihají na malá, zvládnutelná lemmata.
- Týmy mohou paralelně pracovat na různých částech.
- Software hlídá, aby všechny dílky puzzle logicky zapadaly do sebe.
- Výsledný kód slouží jako trvalý a ověřitelný archiv.
Dříve některé velké hypotézy ležely ladem jednoduše proto, že se nikdo neodvážil prohrabat se tisíci řádky úsudků. Dnes roste přesvědčení, že omluva „příliš velké na kontrolu" pomalu mizí. Nástroje jako Lean, Coq a Isabelle z takových projektů dělají splnitelné úkoly — pokud se zapojí dost lidí.
Mathlib: něco jako GitHub pro matematické jistoty
Klíčovou roli hraje mathlib, centrální knihovna systému Lean. Obsahuje již více než 1,2 milionu řádků definic, vět a důkazů — od základní aritmetiky a teorie grup až po pokročilou analýzu.
Kdo chce formalizovat nový důkaz, nemusí budovat vše od nuly. Může se opřít o dříve zaznamenané výsledky, stejně jako programátoři využívají existující softwarové balíčky. To každý nový projekt urychluje a zvyšuje přitažlivost asistentů pro ověřování důkazů.
Pokaždé, když je přidána nová věta, roste hodnota celého ekosystému. Další badatel může začít o krok dál.
Software, který odhaluje chyby v oceněných důkazech
Role těchto systémů se neomezuje jen na potvrzování správnosti. Odhalují také místa, kde lidské uvažování přece jen nesedí. V roce 2021 formalizoval tým v systému Lean dříve oceněnou větu. V půlce práce software odmítl pokračovat: někde chyběl zásadní krok.
Autoři se vrátili k vlastní práci a zjistili, že počítač měl pravdu. Původní článek musel být upraven. Žádný recenzent to nezachytil, přestože v logice zela vážná mezera.
Takové případy udávají tón. Zatímco lidský čtenář si někdy řekne „tahle část bude asi v pořádku", software nezná dobrou vůli. Program přijme krok jedině tehdy, pokud ho doslova dokáže odvodit z předchozích řádků a předpokladů. Jinak se vše zastaví.
| Lidská kontrola | Kontrola s asistentem důkazů |
|---|---|
| Pracuje s intuicí a zkušeností | Pracuje s přísně formálními pravidly |
| Může části přeskočit nebo shrnout | Prochází každý krok bez výjimky |
| Unavuje se, ztrácí soustředění | Zůstává konzistentní i po milionech řádků |
| Ovlivnitelná reputací nebo statusem | Neutrální: rozhoduje pouze logika |
Díky umělé inteligenci se práh vstupu snižuje
Dlouhou dobu byly tyto nástroje výsadou počítačových vědců. Křivka učení byla strmá, jazyk přísný a málo odpouštějící. Matematici bez programátorské zkušenosti brzy vzdávali.
Tento obraz se mění. Nová rozhraní, často s pomocí modelů umělé inteligence, překládají neformální matematiku do formálního kódu Lean. Výzkumník může načrtnout důkaz tak, jak je zvyklý, a asistent navrhne příslušné příkazy v Leanu.
Univerzity zakládají pracovní skupiny, kde doktorandi rovnou budují své důkazy v takovém systému. Zároveň se tak učí moderní matematice i disciplíně přesného formulování každého kroku. Software pak funguje téměř jako přísný vedoucí, který žádné nepřesnosti nepropustí.
Co to znamená pro budoucnost matematiky?
Vzestup asistentů pro ověřování důkazů 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 se rozvíjí hybridní model.
Intuice, kreativita a hledání překvapivých spojitostí zůstávají lidskou doménou; počítač hlídá, aby se výsledné zpracování nikde nevymklo z logických kolejí.
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í zvláštní váhu. Drobná chyba v důkazu bezpečnostního protokolu může učinit zranitelným hardware za miliardy. Firmy i výzkumné instituce proto stále častěji hledají nástroje, které dokážou matematické jistoty garantovat.
Kdo matematiku studuje nebo vyučuje, může tento vývoj využít velmi konkrétně. Formalizace malých vět z analýzy nebo algebry v asistentovi důkazů nutí studenty k přesnému formulování a vynáší na povrch implicitní předpoklady. Vyučující tak získávají přehled o tom, kde uvažování skutečně drhne.
Někomu z vnějšku se může zdát, jako by matematici vyměňovali svou mystiku za nudný kód. Ve skutečnosti se děje něco jiného: intuitivní skoky a kreativní nápady přetrvávají, ale nezmizí v nesrozumitelných rukopisech. Usazují se do podoby, kterou každá příští generace může krok po kroku procházet, ověřovat a rozšiřovat — s počítačem jako neúnavným společníkem při čtení.
