Tam, kde matematici dříve spoléhali na červené tužky a tlusté stohy papíru, si dnes ke stolu přisedá tichý, neúprosný software.
Nové programy kontrolují matematické důkazy řádek po řádku, aniž by se unavily nebo ztratily nit. Přední světové kapacity v oblasti matematiky nechávají své nejsložitější věty ověřovat systémy jako Lean, který odhaluje chyby tam, kde by je žádný člověk vůbec nehledal.
Od osamělého myslitele k matematickému týmu s počítačovými asistenty
Matematika měla po staletí něco samotářského. Badatel se stáhl do ústraní, pracoval léta na důkazu a pak ho poslal malé skupině kolegů. Ti vše pečlivě přečetli, někdy celé měsíce. Nakonec přišlo jakési tiché podání ruky: všichni předpokládali, že vše sedí.
V praxi se ukázalo, že tento přístup je zranitelný. Důkazy moderních vět snadno zaberou stovky stránek. Zapomenutá podmínka, příliš rychlý úsudek, chyba při přepisu — malé přehlédnutí může mít velké následky. Přesto snadno proklouzne, protože téměř nikdo takové dílo nedokáže projít do posledního detailu.
Německý matematik Peter Scholze tento tlak pocítil na vlastní kůži. Získal prestižní Fieldsovu medaili, patří k absolutní světové špičce, a přesto ho trápily pochybnosti ohledně obrovského důkazu týkajícího se takzvaných „kondenzovaných prostorů". Jen hrstka expertů vůbec rozuměla, o čem mluví. Natož aby byl někdo schopen vše důkladně přepočítat.
Veřejný experiment s počítačem v roli rozhodčího
Místo hledání dalších lidských čtenářů zvolil Scholze odlišnou cestu. V roce 2020 spustil takzvaný Liquid Tensor Experiment — otevřenou výzvu matematikům a programátorům, aby jeho práci přeložili do systému Lean, neboli do takzvaného asistenta pro ověřování důkazů.
Takový asistent není kalkulačka, nýbrž přísný účetní logiky. Uživatel zapíše důkaz ve formálním jazyce. Software pak zkontroluje každý krok: plyne tento závěr skutečně z předchozího, v souladu s dohodnutými axiomy a definicemi? Pokud ne, systém odmítne pokračovat. Žádné nadržování, žádná pověst — jen čistá konzistence.
Po celém světě se výzkumníci vrhli na Scholzeho výzvu. Místo jednoho izolovaného génia s poznámkovým blokem vzniklo online staveniště: desítky lidí pracovaly na malých částech téhož důkazu. Lean a centrální knihovna mathlib přitom hlídaly celkovou soudržnost.
Po šesti měsících existovalo 180 000 řádků kódu v jazyce Lean — dostatečný základ pro formální potvrzení, že Scholzeova věta obstojí bez logických mezer.
Pro Scholzeho to bylo jiné ujištění než tradiční peer review. Ne „nikdo zatím 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ě neproveditelné megaprojekty se najednou stávají realizovatelnými
Scholzeho příběh není ojedinělý. V roce 2016 vyřešila Maryna Viazovska staletý hlavolam: jak co nejefektivněji uložit koule v osmi dimenzích? Její řešení bylo celosvětově oslavováno a v roce 2022 jí vyneslo také Fieldsovu medaili.
Přesto byl s tím spojen jeden praktický problém. Její důkaz je zapsán neobyčejně kompaktně, avšak je konceptuálně a technicky tak náročný, že důkladná lidská kontrola trvá roky. Riziko, že nějaký detail zůstane skrytě chybný, je reálné.
Mezinárodní skupina výzkumníků se proto rozhodla formalizovat její práci v Lean, podobně jako u Scholzeho. Měsíce pracovali na digitální verzi jejího postupu. V roce 2024 se objevil kompletní kód, volně přístupný k nahlédnutí. Lean prošel vším a potvrdil, že struktura důkazu je bezchybná.
- Obrovské důkazy se rozstříhají 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 dohromady.
- Výsledný kód slouží jako trvalý, ověřitelný archiv.
Dříve některé velké domněnky zůstávaly nevyřešeny jednoduše proto, že nikdo neměl odvahu prohledat tisíce řádků argumentace. Nyní 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 dnes obsahuje přes 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 začátku. Opírá se o dříve zaznamenané výsledky, podobně jako programátoři využívají existující softwarové balíčky. Každý nový projekt se tím urychluje a asistenti pro ověřování důkazů se stávají atraktivnějšími.
Pokaždé, když je do systému přidána nová věta, roste hodnota celého ekosystému. Příští výzkumník může začít o krok dál.
Software, který odhaluje chyby v oceňovaných důkazech
Úloha těchto systémů se neomezuje pouze na potvrzování správnosti. Dokážou také ukázat, kde lidské uvažování přece jen nesedí. V roce 2021 formalizoval jeden tým dříve oceněnou větu v jazyce Lean. Uprostřed procesu software odmítl pokračovat: někde chyběl zásadní krok.
Autoři se znovu ponořili do vlastní práce a zjistili, že počítač měl pravdu. Jejich původní článek musel být opraven. Žádný recenzent to neodhalil, přestože v logice zela vážná mezera.
Podobné případy udávají tón. Zatímco lidský čtenář si někdy myslí „tahle část bude asi v pořádku", software nic takového nezná. Program přijme krok jedině tehdy, pokud ho dokáže doslova odvodit z předchozích řádků a předpokladů. Jinak se vše zastaví.
| Lidská kontrola | Kontrola s asistentem pro důkazy |
|---|---|
| Pracuje s intuicí a zkušeností | Pracuje s přísně formálními pravidly |
| Může části přeskočit nebo shrnout | Projde každý krok bez výjimky |
| Unaví se, ztrácí koncentraci | Zůstává konzistentní i po milionech řádků |
| Ovlivnitelný pověstí nebo statusem | Neutrální: rozhoduje pouze logika |
Díky umělé inteligenci se práh přístupu snižuje
Po dlouhou dobu byly tyto nástroje doménou především 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ých zkušeností brzy vzdali.
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 mu pak nabídne odpovídající příkazy v Leanu.
Univerzity zakládají pracovní skupiny, kde doktorandi budují své důkazy přímo v takovém systému. Učí se přitom moderní matematiku i disciplínu přesně formulovat každý krok. Software pak funguje téměř jako přísný vedoucí, který nepromíjí žádnou nedbalost.
Co to znamená pro budoucnost matematiky?
Nástup 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 myšlenkou, nebo stroj, který prokáže, že každá část logicky drží? V praxi se rozvíjí hybridní model.
Intuice, kreativita a nalézání překvapivých souvislostí zůstávají lidskou doménou; počítač hlídá, aby se zpracování nikde nevymklo z logického rámce.
V oborech, kde matematika přímo přechází do techniky — jako je kryptografie, konstrukce letadel nebo výroba čipů — získává formální ověřování zvláštní váhu. Malá chyba v důkazu bezpečnostního protokolu může zranitelnosti vystavit zařízení v hodnotě miliard. Firmy i výzkumné instituce se proto stále více ohlížejí po nástrojích, které dokážou matematické jistoty garantovat.
Kdo matematiku studuje nebo vyučuje, může tento vývoj využít velmi konkrétně. Formalizace menších tvrzení z analýzy nebo algebry v asistentovi pro důkazy nutí studenty přesně formulovat myšlenky a vynáší na povrch implicitní předpoklady. Vyučující tak získávají přehled o tom, kde uvažování skutečně vázne.
Pro nezasvěcené to možná vypadá, 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 zůstávají, ale již nezmizí v neprostupných rukopisech. Usazují se ve formě, kterou každá příští generace může krok za krokem projít, ověřit a rozvinout dál — s počítačem jako neúnavným spolučtenářem.
