OpenAI tvrdí, že interní Astra našla řešení deseti dlouho otevřených matematických problémů
OpenAI zveřejnilo Lean 4 formalizace deseti výsledků, které podle firmy vznikly pomocí interního systému Astra. Simon Willison upozorňuje na chybějící informace o neúspěšných pokusech.
OpenAI oznámilo deset výsledků v matematice a teoretické informatice, na kterých podle firmy pracoval interní systém Astra. Firma uvádí, že vybrala problémy bez významného pokroku na hlavním výsledku nejméně deset let.
OpenAI tvrdí, že každý úspěšný běh stál při cenách GPT-5.6 Sol méně než 2 000 dolarů. Toto číslo ale neříká, kolik neúspěšných běhů, pokusů o výběr problému nebo lidské práce celému výsledku předcházelo. Simon Willison na tuto chybějící informaci výslovně upozorňuje.
Firma zveřejnila Lean 4 formalizace v repozitáři openai/ten-proofs. Ty umožňují strojově zkontrolovat formalizované části důkazů. Nezveřejňují ale automaticky kompletní historii promptů, výzkumných rozhodnutí ani neúspěšných experimentů.
Je proto přesnější psát, že OpenAI tvrdí, že Astra našla řešení, než bez dalšího ověření říkat, že model definitivně vyřešil deset otevřených problémů.
Původní článek spojoval toto oznámení s odlišným výzkumem Anthropicu v kryptografii a s obecnými komentáři matematiků. Tyto body vyžadují vlastní primární zdroje a nejsou součástí krátkého zdroje Simona Willisonse k deseti výsledkům OpenAI.
Zveřejněné formalizace jsou důležitým podkladem pro další kontrolu. Teprve nezávislé posouzení matematiky ukáže, jak nový a významný je každý z deseti výsledků.