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.
Kaž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ý.
Šé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.