AI prý vyvrátila hypotézu exponenciálního času. Co je opravdu ověřeno a co zatím ne

Hypotéza exponenciálního času (anglicky Exponential Time Hypothesis, zkráceně ETH) není nic, o čem by se mluvilo u oběda. Pro teoretickou informatiku je ale stejně důležitá jako nosná zeď v domě. Od roku 1999, kdy ji formulovali Russell Impagliazzo a Ramamohan Paturi, na ní stojí stovky výsledků o tom, které úlohy počítače rychle vyřešit nedokážou.

Koncem října 2026 ohlásily OpenAI i Anthropic, že jejich modely tuto hypotézu vyvrátily, nezávisle na sobě a téměř ve stejný den. Oba důkazy prošly strojovou kontrolou v systému Lean. Přesto žádný uznávaný odborník zatím neřekl „je to ověřené“. V článku vysvětlujeme proč.

Vycházíme z článků a Lean repozitářů obou firem, z oznámení OpenAI, ze zprávy časopisu Science, z blogu, který k výsledku založili sami autoři ETH, a z nezávislých kontrol. Stav jsme ověřili 2. 11. 2026.

Ve zkratce

• Co je ETH: předpoklad, že úlohu 3-SAT (splnitelnost logické formule) nejde v nejhorším případě vyřešit v čase, který roste pomaleji než exponenciálně, tedy v čase 2^o(n).
• OpenAI zveřejnila 26. 10. 2026 článek The Exponential Time Hypothesis is False. Anthropic týž den článek A 2^o(n) Time Algorithm for 3-SAT, jehož autorem je uveden „Claude (Anthropic)“.
• Oba přístupy přinášejí deterministický algoritmus, který spočítá všechna řešení k-SAT formule v čase zhruba 2^O(n·log log n / √log n).
• Lean ověřil důkazy formálních tvrzení. Neověřil ale, že formální tvrzení přesně odpovídají učebnicové ETH. To musí zkontrolovat lidé.
• Praktický dopad je nulový. Algoritmus porazí hrubou sílu až u formulí s astronomickým počtem proměnných. Šifrování ani otázky P vs. NP se to netýká.
• Lidskou kontrolu vedou Impagliazzo, Paturi a Ryan Williams. Sami zdůrazňují, že jejich účast není potvrzením správnosti.

Co přesně je hypotéza exponenciálního času

Představte si logickou formuli s n proměnnými, z nichž každá může být pravda, nebo nepravda. Úloha 3-SAT se ptá, jestli existuje přiřazení hodnot, které formuli splní. Hrubou silou zkusíte všech 2^n možností. Chytřejší algoritmy byly rychlejší, ale stále exponenciální: podle článku Anthropicu byl dosavadní rekord zhruba 1,328^n pro deterministické a 1,308^n pro náhodnostní algoritmy.

ETH tvrdí, že to principiálně líp nejde: že neexistuje algoritmus s během 2^o(n), tedy takový, jehož čas roste pomaleji než jakákoli exponenciála c^n s c > 1. Hypotéza nikdy nebyla dokázaná. Výzkumníci ji ale používali jako pracovní předpoklad a odvozovali z ní, jak rychle se dají (nebo nedají) řešit tisíce dalších úloh. Literární rešerše Clauda podle Anthropicu našla přes 800 prací, které se o ETH nebo silnější hypotézu opírají.

Co tvrdí OpenAI a co Anthropic

OpenAI výsledek zveřejnila 26. 10. 2026 společně se dvěma dalšími: o lokálním vyhlazování vlnové rovnice (spojené s Kakeyovou hypotézou) a o problému Yangovy–Millsovy teorie. Podle firmy model důkaz ETH našel 16. 10. a o den později byla hotová formalizace v Leanu. Článek popisuje deterministické počítání řešení k-CNF formulí v čase 2^O(n log log n / √log n) s polynomiální pamětí. Tvrdí, že tím padá ETH i její silnější varianty (SETH, Gap-ETH a NSETH). Formalizace v Leanu přitom pokrývá o něco slabší odhad, n·(log log n)² / √log n v exponentu, který na vyvrácení ETH také stačí.

Anthropic zveřejnil vlastní článek a Lean 4 formalizaci ve svém repozitáři formal-math. Hlavní algoritmus podle firmy našel 16. 10. interní výzkumný model Claude, „se 14 miliony výstupních tokenů a bez lidského vstupu“. Na podobě článku pak s Claudem pracovali výzkumníci. Odhad času je 2^O(min{k² n log log n / √log n, k m / √log m}), kde m je počet klauzulí. V repozitáři firma výslovně píše, že výsledek je „čistě asymptotický a o řešení formulí v praxi neříká nic“.

Že dva týmy dospěly k podobnému výsledku ve stejný den, je samo o sobě pozoruhodné. Neplatí to ale jako nezávislé ověření: oba důkazy dosud prošly jen strojovou kontrolou, ne lidským posouzením.

Co ověřil Lean a co ne

Lean je takzvaný dokazovač vět. Program, který krok po kroku kontroluje, že z daných předpokladů opravdu plyne dané tvrzení. Pokud Lean důkaz přijme, chyba v logice důkazu je velmi nepravděpodobná.

Háček je jinde. Lean kontroluje důkaz formálního zápisu tvrzení, ne to, co si pod ním představuje člověk. Anthropic to v repozitáři přiznává otevřeně: soubor s hlavními tvrzeními je krátký právě proto, aby si čtenář mohl sám ověřit, že říká totéž co článek, protože „žádný stroj nekontroluje, že tento soubor říká, co říká článek“.

Nezávislý vývojář Carlos Toledo oba Lean důkazy přehrál a jádra je přijala jen se standardními axiomy. Sám ale upozorňuje, že to „neosvědčuje, že ETH neplatí“. Ověřil jen soulad důkazů s jejich formálními tvrzeními. Otevřená zůstává otázka, zda tato tvrzení přesně vystihují ETH a výpočetní model, který se v teorii složitosti používá.

Co říkají odborníci

• Holger Dell (IT University of Copenhagen) řekl časopisu Science: „Je jasné, že jde o zásadní průlom.“
• Russell Impagliazzo, spoluautor ETH, je opatrnější: „Pokud jde o mě, není to stoprocentně jisté.“ První verze od OpenAI byla podle něj „naprosto nečitelná“ a tým ji deset dní přepisoval.
• Ryan Williams (MIT) upozorňuje, že stovky prací založených na ETH „nejsou mrtvé“. Bude ale potřeba je přestavět na bezpečnějších předpokladech.
• Lance Fortnow na blogu Computational Complexity napsal, že důkaz sám neověřoval, ale „dá se bezpečně předpokládat, že hypotéza exponenciálního času je odepsaná“.

Proč to nemá vliv na šifrování ani praxi

Titulky typu „AI rozbila základ informatiky“ svádějí k představě, že se něco změní v reálném světě. Nezmění. Podle článku Anthropicu nový algoritmus pro formule s m = 5n klauzulemi porazí hrubou sílu až při víc než 10^10 000 proměnných. Odhad, který závisí jen na n, dokonce až nad 10^(10^8). Zároveň autoři odhadují, že tento přístup nejspíš nepřekoná hrubou sílu u formulí s méně než 10^7 proměnnými, přičemž hrubá síla je nepoužitelná už při 100 proměnných.

Výsledek neřeší otázku P vs. NP. Algoritmus je stále superpolynomiální. Podle Anthropicu nevyvrací ani hypotézu ortogonálních vektorů, další pilíř takzvané jemnozrnné složitosti. Na šifrování, které stojí na jiných předpokladech, nemá přímý dopad.

Pro obor je to přesto velká věc: stovky podmíněných výsledků ztrácejí oporu a některé teoretické důsledky naopak přibývají. Anthropic uvádí například, že třída E^NP nemá obvody lineární velikosti.

Jak firmy výsledek zveřejnily a proč to vadí

OpenAI vybrala tři odborníky, kteří kontrolu ETH „vedou“: Ryana Williamse a oba autory hypotézy, Impagliazza a Paturiho. Podle firmy nepodepsali smlouvu o mlčenlivosti ani nedostali zaplaceno. OpenAI slíbila financovat odbornou konferenci. Trojice založila veřejný blog ETH: Community Examination and Discussion a hned v prvním příspěvku napsala: „Naše účast nesmí být chápána jako potvrzení tvrzení.“ Blog postupně přidal odkazy na srozumitelnější výklady (Mark Sellke, Ryan O’Donnell, Shiva Kintali), vlákno o replikacích v Leanu a 1. 11. výzvu, aby lidé hlásili výsledky, které z vyvrácení plynou.

Kritika míří jinam. Podle Science se poradní skupina AGMAI (Advisory Group on Mathematics and AI) ohradila proti tomu, že si firma sama vybírá, kdo bude výsledek posuzovat. Vyzvala také ke zveřejnění důkazu k Yangově–Millsově teorii (1147 stran), který zatím drží komise pod vedením nositele Nobelovy ceny Davida Grosse. Williams sám kritizuje, že o tom, kdo se ujme kontroly, rozhoduje firma. Další plánované kroky jsou pracovní skupina na lidsky čitelný důkaz, virtuální konference ještě do konce roku 2026 a možná prezenční setkání v roce 2027.

Poučení z Hodgeovy hypotézy

Opatrnost má konkrétní důvod. 6. 10. 2026 OpenAI zveřejnila tři články k Hodgeově hypotéze, jednomu z velkých otevřených problémů matematiky. Do dvou dnů je stáhla. Matematik Nathan Humphrey 7. 10. upozornil na chybu ve znaménkové konvenci a při hledání pracoval s Claudem i s modelem GPT. Zdroj chyby pak rozebrali Yankı Lekili (Imperial College London) a Nick Sheridan (Univerzita v Edinburghu) v článku na arXivu. Hodgeovy články přitom neměly formalizaci v Leanu. Oznámení o stažení dodává, že netvrdí, že by matematické tvrzení samo bylo nepravdivé.

U ETH je situace lepší: existují dvě nezávislé formalizace a obě prošly kontrolou. Kdo ale z Hodge vyvozuje, že „model to řekl, tak to platí“, by měl počkat na lidský verdikt.

Co bude dál

• Lidská kontrola pokračuje na blogu autorů ETH a v pracovní skupině, která má připravit čitelný důkaz.
• Do konce roku 2026 se má konat virtuální konference, kde se výsledek posoudí veřejně.
• Klíčová otázka zní, zda formální tvrzení v Leanu přesně odpovídají učebnicové ETH. Pokud ano, je hypotéza po 27 letech vyvrácená.

Pro běžné uživatele z toho plyne jednodušší poučení: AI dnes umí v matematice víc, než se čekalo, ale „model to dokázal“ ještě neznamená „je to pravda“. Proč je dobré si i v běžné práci ověřovat, co AI tvrdí, vysvětlujeme v článku Proč AI vymýšlí.