Astra od OpenAI vyřešila deset otevřených matematických problémů. Za 2000 dolarů API tokenů

OpenAI oznámila 2. srpna 2026 novou generaci modelů pod pracovním názvem Astra. Místo klasického press releasu s benchmarky publikovala 249stránkový sborník matematických důkazů, kde její interní verze vyřešila desítku problémů, které matematici otevírali dekády. Celkový compute cost: zhruba 2 000 dolarů API tokenů. Zatím si to nekoupíš, ale je to nejkonkrétnější náhled, kam AI míří v oblasti vědeckého výzkumu.

01KapitolaCo OpenAI oznámila

Astra je pracovní název další velké rodiny modelů OpenAI. Firma ji zatím nespustila v ChatGPT ani přes API a nezveřejnila, jestli půjde jako GPT-6 nebo jako další varianta pětky. Místo blogpostu s marketingovými čísly OpenAI vydala report a přiložený manuskript, kde interní Astra vyřešila deset otevřených problémů z matematiky a teoretické informatiky.

Konkrétní výčet: explicitní konstrukce ne-sofic grupy (otázka otevřená od roku 1999, kdy pojem soficity zavedl Mikhail Gromov), vyvrácení Connesovy rigidity conjecture, Ehrhartova volume conjecture, tři Erdősovy problémy z multibarevných Ramseyho čísel a extremal graph theory, sphere packing bounds, binary a spherical kódy, arithmetic circuit complexity, kvantová parallel repetition a closest vector problem v lattice kryptografii. Každý důkaz je zformalizovaný v Lean 4, certifikáty jsou na GitHubu pod Apache 2.0. Repozitář hlásí nulu nedokončených kroků (Lean tomu říká sorry), tedy každou dedukci vidí typový systém od axiomů po závěr. Celkový compute na všech deset řešení dohromady vyšel na zhruba 2 000 dolarů v cenách API pro GPT-5.6 Sol.

02KapitolaProč tě zajímá model, který si zatím ani nekoupíš

Krátká odpověď: běžné práci ti Astra nepomůže, ale mění, jak si máš plánovat rok dopředu. Poprvé máš od velké laboratoře vědecký výstup, který ti nemusí prodávat marketingový tým. Máš ho ověřený strojem.

Lean 4 je typový systém, který sám kontroluje, že každý krok důkazu logicky navazuje. Když projde kompilátor bez sorry, důkaz platí. Není o čem diskutovat, ověří ti to laptop za pár minut. To je jiná situace než loňské říjnové oznámení, že GPT-5 vyřešil Erdősovy problémy. Tam se za týden ukázalo, že model retrievoval existující řešení bez originálního přínosu. U Astry je manipulace vyloučená, protože každý si můžeš stáhnout repozitář a spustit lean lokálně.

Druhá věc, kterou si stojí zapamatovat, je cena. Dva tisíce dolarů API za deset dekády otevřených výsledků je zlomek toho, co stojí jeden článek v Nature nebo Annals of Mathematics. Vědecký výzkum přestává být svázaný jen s časem člověka. Compute jde nakoupit a Noam Brown z OpenAI přímo přiznává, že tým na jednotlivé problémy nepálil neomezené zdroje. Pushnout test-time compute dál je otevřená možnost.

03KapitolaKdo z toho reálně bude něco mít

Zatím nikdo z běžných uživatelů ChatGPT. Astra není v žádném produktu, na který by ses proklikl. Ale tři skupiny by měly začít přemýšlet, co s tím.

Vědci a matematici jsou první. Kdo dnes na univerzitě řídí PhD studenty nebo postdoky, musí počítat s tím, že AI umí formalizovat důkaz do Lean 4 za pár set dolarů. Změní se ekonomika toho, čemu se dnes říká otevřený problém. Když se dá zaplatit compute a dostat důkaz, přehodnotí se, čemu se říká "nedosažitelný" a čemu jen "otevřený" problém.

Druhou skupinou jsou týmy, které dělají formal verification softwaru. Kdo pracuje s Lean, Coq nebo F* na verifikaci kryptografie, kompilátorů nebo bezpečnostních protokolů, dostane během roku nástroj, který sám dopisuje důkazy invariantů. Astra ještě není v public API, ale schopnost je tam. Jakmile ji OpenAI otevře, formal verification přestane být disciplína pro dvě stě lidí v Cambridge, Paříži a Bostonu.

Třetí skupina jsou vývojáři a analytici, kteří sledují, kam se posouvá test-time compute. Když dnes stačí 2 000 dolarů na deset PhD-level důkazů, za rok to bude řádově méně. Kdo staví AI pipeline nebo pracuje s agenty, měl by počítat s tím, že úlohy, které se dnes zdají nedostupné, budou letos nebo příští rok běžně řešitelné přes standardní API.

04KapitolaJak si ověřit, že důkaz skutečně sedí

Nemusíš věřit OpenAI ani modelu. Astra důkazy jsou publikované, kdokoli s Linuxem nebo macOS je zvládne ověřit za odpoledne. Postup:

Tenhle postup je klíč k tomu, proč Astra oznámení sedí jinak než dřívější "AI vyřešila X". Lean neumí halucinovat. Buď důkaz projde, nebo ne. Když projde, ztrácí smysl hádka o schopnostech modelu. Umí to.

Příklad z praxe

Kryptografický tým, který dělá lattice-based algoritmy pro post-quantum standard, dostal od kolegy tip na jeden ze zveřejněných Astra důkazů, konkrétně na výsledek k closest vector problem. Místo dlouhého čekání na peer review v oborovém časopise stáhli repozitář, pustili Lean kompilátor a za hodinu měli jistotu, že důkaz sedí. Následně z něj vytáhli lemma, které použili v bezpečnostní analýze vlastního návrhu. Cena za ověření nula dolarů, protože OpenAI dala výsledek pod otevřenou licenci a hardware měl tým už doma.

05KapitolaShrnutí

Astra ještě nekoupíš, ale je to nejkonkrétnější doklad, že AI zvládá originální vědecký výzkum se strojově ověřitelným výstupem. Deset otevřených matematických problémů, Lean 4 certifikáty s nulou sorry, celková cena 2 000 dolarů API. První krok pro tebe: podívej se na Astra repozitář na GitHubu, vyber si jeden důkaz a projeď ho lokálně. Uvidíš na vlastní oči, jak vypadá výstup, který za rok dostane přes běžné API každý, kdo zaplatí.

06KapitolaZdroje

• SiliconANGLE: OpenAI's Astra solves 10 long-open math problems and publishes the proofs, 2. srpna 2026.
• The Decoder: OpenAI announces its "next major model" Astra by dropping ten previously unsolved math solutions, srpen 2026.
• DataCamp: OpenAI's New Model, Astra, Has Solved Ten Open Math Problems, srpen 2026.
• Quartz: OpenAI Astra model solves 10 open math problems for $2,000, 3. srpna 2026.
• Forbes: OpenAI's Astra Solved Decades-Old Math Problems For $2,000, 3. srpna 2026.