{"data":{"id":2195,"lang":"cs","title":"Nezveřejněný model Astra od OpenAI vyřešil deset desítky let starých matematických problémů","summary":"OpenAI tvrdí, že interní verze jejich nezveřejněného modelu Astra vyřešila deset desítky let starých matematických problémů a zveřejnila strojově ověřené důkazy v systému Lean za přibližně 2 000 dolarů výpočetního výkonu.","category":"ai","category_label":"AI","published_at":"2026-08-03T06:02:12Z","updated_at":"2026-08-03T06:02:12Z","url":"https://techtools.cz/tools/news/clanek/2195-nezverejneny-model-astra-od-openai-vyresil-deset-desitky-let-starych","api_url":"https://techtools.cz/news-api/v1/articles/2195?lang=cs","markdown_url":"https://techtools.cz/news-api/v1/articles/2195.md?lang=cs","image_url":"https://d15shllkswkct0.cloudfront.net/wp-content/blogs.dir/1/files/2026/08/openaiatramaths.png","word_count":239,"reading_time_minutes":2,"sources":[{"url":"https://thenextweb.com/news/openai-astra-model-ten-math-proofs-non-sofic-groups","domain":"thenextweb.com"},{"url":"https://siliconangle.com/2026/08/02/openais-astra-solves-10-long-open-math-problems-publishes-proofs/","domain":"siliconangle.com"}],"translation":{"lang":"en","id":2122,"title":"OpenAI's Unreleased Astra Model Solves Ten Decades-Old Math Problems","url":"https://techtools.cz/tools/news/article/2122-openai-s-unreleased-astra-model-solves-ten-decades-old-math-problems","api_url":"https://techtools.cz/news-api/v1/articles/2122?lang=en"},"content":"OpenAI 1. srpna oznámila, že interní verze modelu Astra, jejich připravované příští velké modelové rodiny, vyřešila deset otevřených problémů z matematiky a teoretické informatiky, z nichž každý zůstával nevyřešený nejméně deset let. Hlavním výsledkem je první explicitní konstrukce nesofické grupy, čímž se uzavřela otázka otevřená od roku 1999, kdy tento pojem zavedl matematik Michail Gromov. Model dále vyvrátil Connesovu rigidity hypotézu o von Neumannových algebrách, dokázal Ehrhartovu objemovou hypotézu a vyřešil tři Erdősovy problémy, včetně jednoho o vícebarevných Ramseyho číslech.\n\nKe každému výsledku je přiložen strojově ověřitelný certifikát v systému Lean 4, zveřejněný na GitHubu pod licencí Apache 2.0 spolu s 249stránkovým rukopisem. Repozitář hlásí nulový počet neověřených kroků („sorry count“ nula) — tedy žádný krok v žádném z deseti formálních důkazů nezůstává neověřený. Důvěryhodné jádro systému Lean dává binární verdikt „projde, nebo ne“, který nevyžaduje žádný pokročilý titul ke kontrole. OpenAI uvádí, že celá práce stála přibližně 2 000 dolarů na výpočetní výkon podle sazeb jejich API GPT-5.6 Sol.Sebastien Bubeck, vedoucí matematického výzkumu OpenAI, označil výsledky za „nádherné“ a držitel Fieldsovy medaile Timothy Gowers uvedl, že by jeden z důkazů bez váhání doporučil k publikaci v předním časopise. Thomas Bloom, správce databáze erdosproblems.com, označil zprávu za významnou a upozornil na kontrast s dřívějšími matematickými tvrzeními OpenAI z října 2025, která byla později stažena. Žádný z deseti výsledků zatím neprošel formálním recenzním řízením a OpenAI zatím neuvedla datum vydání, cenu ani podrobnosti o přístupu k API pro samotný model Astra."}}