Il 2 agosto 2026 OpenAI ha reso pubblici dieci problemi aperti di matematica e informatica teorica — alcuni fermi da oltre vent'anni, incluso uno rimasto irrisolto dal 1999 — risolti da Astra, un modello ancora non rilasciato. Il costo computazionale dichiarato è di circa 2.000 dollari. Ogni soluzione è accompagnata da un certificato formale in Lean 4, pubblicato su GitHub: il conteggio dei passaggi non dimostrati ("sorry") è zero, il che garantisce che ogni riga della prova sia verificata da un compilatore, non da un revisore umano. Le reazioni della comunità matematica sono state caute: nell'ottobre 2025 la stessa azienda aveva annunciato di aver risolto dieci problemi del catalogo di Erdős, salvo scoprire — grazie a Thomas Bloom, curatore del database erdosproblems.com — che si trattava di soluzioni già pubblicate e mai catalogate; il post venne cancellato. Questa volta è stato lo stesso Bloom a validare pubblicamente i nuovi risultati. Resta un punto sollevato da più matematici, tra cui Henry Yuen (che ha lavorato anni a uno dei problemi risolti) e il critico Fernando Borretti: la dimostrazione formale garantisce la correttezza logica, non la comprensibilità umana del ragionamento. Il paper stesso, secondo Yuen, lascia le parti tecnicamente più interessanti sepolte in fondo al testo. La domanda che resta aperta non è se il risultato sia vero, ma chi — in futuro — sarà ancora in grado di seguirne il perché.