{"data":{"id":2322,"lang":"cs","title":"Nezveřejněný model Astra od OpenAI vyřešil 10 otevřených matematických problémů za 2000 dolarů","summary":"Interní model OpenAI jménem Astra vytvořil deset strojově ověřených důkazů desítky let starých otevřených matematických problémů za přibližně 2000 dolarů výpočetních nákladů.","category":"ai","category_label":"AI","published_at":"2026-08-25T02:01:18Z","updated_at":"2026-08-25T02:01:18Z","url":"https://techtools.cz/tools/news/clanek/2322-nezverejneny-model-astra-od-openai-vyresil-10-otevrenych-matematickych-problemu","api_url":"https://techtools.cz/news-api/v1/articles/2322?lang=cs","markdown_url":"https://techtools.cz/news-api/v1/articles/2322.md?lang=cs","image_url":"https://media.thenextweb.com/2026/08/openai-astra-model-ten-math-proofs-non-sofic-groups.avif","word_count":192,"reading_time_minutes":1,"sources":[{"url":"https://www.implicator.ai/openai-astra-10-math-problems-lean-proofs/","domain":"implicator.ai"},{"url":"https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups","domain":"thenextweb.com"}],"translation":{"lang":"en","id":2249,"title":"OpenAI's Unreleased Astra Model Solves 10 Open Math Problems for $2,000","url":"https://techtools.cz/tools/news/article/2249-openai-s-unreleased-astra-model-solves-10-open-math-problems-for-2-000","api_url":"https://techtools.cz/news-api/v1/articles/2249?lang=en"},"content":"OpenAI oznámila, že interní, dosud nezveřejněný model Astra vytvořil ověřená řešení deseti problémů z matematiky a teoretické informatiky, které zůstávaly nevyřešené deset a více let. Mezi výsledky patří první explicitní konstrukce nesofické grupy — otázka otevřená od roku 1999 — vyvrácení Connesovy hypotézy o rigiditě a první zlepšení odhadů hustoty sferického balení od roku 1978.\n\nKaždé řešení bylo doprovázeno strojově ověřitelným certifikátem důkazu v systému Lean 4, zveřejněným na GitHubu, takže matematici mohou logiku ověřit krok po kroku, aniž by museli věřit tvrzením OpenAI. Výzkumníci nechali Astru navrhnout argumenty a poté je formalizovali v Leanu; doprovodný rukopis má 249 stran a počet „sorry“ (Leanova značka pro nedokázané mezery) v GitHub repozitáři je nulový.\n\nŠéf matematického výzkumu OpenAI Sebastien Bubeck označil výsledky za „nádherné“, zatímco výzkumník Noam Brown poznamenal, že laboratoř na jednotlivé problémy nevynaložila mnoho prostředků, s žertem, že zatím „žádné z Millenniových problémů“ vyřešeny nebyly. Celkové výpočetní náklady na všech deset řešení činily zhruba 2000 dolarů při současných cenách API. Samotná Astra zůstává nedostupná pro veřejné testování a oznámení přichází uprostřed napětí s matematickou komunitou kvůli tomu, že AI laboratoře zveřejňují výsledky formou blogových příspěvků místo recenzovaných publikací, jak upozorňuje červnová Leidenská deklarace."}}