OpenAI Astra: la scheda in anteprima
Il 1 agosto 2026 OpenAI ha presentato in anteprima la sua prossima grande famiglia di modelli — Astra — non con un keynote o una pagina di lancio, ma pubblicando su un repository GitHub pubblico dieci dimostrazioni formalizzate in Lean 4 di problemi precedentemente irrisolti in matematica e informatica teorica. Non c'è API, non c'è prezzo, non c'è alcuna superficie su ChatGPT e nessuna data di rilascio. Ogni guida all'acquisto "Astra vs GPT-5.6" o "Astra vs Claude" che leggerai questa settimana è speculazione travestita da giornalismo.
Questa pagina è la scheda onesta per chi usa Claude: cosa è davvero confermato, cosa non lo è e se dovrebbe cambiare qualcosa in quello che stai facendo oggi.
- Capire l'esatto meccanismo dell'annuncio e cosa OpenAI ha detto (e NON ha detto) il 1 ago 2026
- Leggere i dieci problemi risolti da Astra e capire perché matematica/TCS è stata scelta come superficie di rivelazione
- Separare i fatti confermati (multi-agente, long-horizon, solo interno) dalle speculazioni (dimensione contesto, prezzi, rollout ChatGPT, benchmark)
- Decidere se continuare a costruire oggi su Claude Opus 5 / Fable 5, oppure aspettare — con una regola pratica concreta
La versione in una frase
Astra è il modello di nuova generazione di OpenAI, solo interno, multi-agente, long-horizon, rivelato attraverso dieci dimostrazioni matematiche verificabili in Lean; non coincide con GPT-5.6 Sol / Terra / Luna e non ha alcuna superficie di prodotto — quindi ogni decisione di migrazione che prendi questo mese è ancora una decisione tra Claude, GPT-5.6 e Gemini 3.6, non su Astra.
Cosa ha detto davvero OpenAI (e cosa no)
La divulgazione è insolita: OpenAI ha annunciato il suo "prossimo modello principale" nel terzo paragrafo di un post di ricerca, senza comunicato stampa, senza benchmark, senza disponibilità e senza prezzi. Quella cornice ti dice tanto quanto il modello stesso — dice "non è ancora un prodotto, è ancora sotto revisione regolatoria".
Confermato il 1 agosto 2026
- Astra è un nome di famiglia di modelli. OpenAI la descrive come "il nostro prossimo modello principale". Si affianca — non è dentro — ai tier Sol / Terra / Luna di GPT-5.6.
- I risultati arrivano da una versione interna. Non l'app ChatGPT, non l'API, non un checkpoint solo-partner.
- La superficie di rivelazione è matematica + TCS. Dieci problemi precedentemente irrisolti, ciascuno con una dimostrazione in Lean 4 pubblicata su
github.com/openai/ten-proofssotto Apache-2.0. - Il sistema è multi-agente e long-horizon. La descrizione di OpenAI è che Astra è "progettato per coordinare più agenti che lavorano insieme su compiti a lungo termine, per ore o giorni", mirato a ricerca, coding e problemi scientifici.
- Ancoraggio di costo (non prezzo del modello). OpenAI ha scritto che i token usati per generare le dieci soluzioni "sarebbero costati circa $2.000 alle tariffe API di Sol". Questo non è il prezzo di listino di Astra, né il costo per dimostrazione, né una garanzia di riproducibilità — è un ancoraggio del volume di token calcolato sul contatore di un altro modello.
- Percorso di revisione governativa. Sam Altman ha mostrato il sistema a funzionari federali statunitensi a Washington, D.C., a fine luglio 2026. Il reporting posiziona Astra come probabile primo modello sottomesso al nuovo quadro normativo USA che richiede la revisione federale prima del rilascio pubblico.
- Citazione ufficiale. Il ricercatore OpenAI Noam Brown ha definito Astra "un passo importante per il ragionamento scientifico" e ha aggiunto: "purtroppo, nessun Problema del Millennio (per ora)".
Non confermato, nonostante quello che potresti leggere
- Nessuna data di rilascio. Nessun calendario di rollout su ChatGPT, nessuna GA API, nessuna beta signup.
- Nessun prezzo. Non per token, non per esecuzione, non per tier.
- Nessuna dimensione della finestra di contesto, nessun output massimo.
- Nessuna dichiarazione multi-modale. Nulla è affermato su immagine, audio o video.
- Nessun benchmark testa-a-testa. Nessun SWE-Bench, nessun ARC-AGI, nessun numero Frontier-Bench.
- Nessuna risposta alla domanda "è GPT-6?". OpenAI non ha detto se Astra uscirà come GPT-6, come un'altra point release GPT-5.x, o con il proprio nome.
- Nessuna conferma della struttura a tier. Lo schema Sol/Terra/Luna di GPT-5.6 non è stato mappato su Astra.
Se un titolo questa settimana ti dà come un fatto una delle voci qui sopra, quell'articolo sta speculando.
Le dieci dimostrazioni, in una schermata
Scegliere di rivelare Astra tramite dimostrazioni formalizzate in Lean 4 su problemi aperti fa molto lavoro: permette a OpenAI di formulare un'affermazione di capacità che è verificabile a macchina, non un numero di leaderboard che si può manipolare. Se le dimostrazioni verificano con lake build All, la tesi matematica è reale indipendentemente da cosa pensi del modello.
| # | Problema | Campo |
|---|---|---|
| 1 | Miglioramento dei limiti asintotici superiori per la densità di sphere-packing | Geometria in alta dimensione |
| 2 | Limiti superiori esponenzialmente più forti per codici binari | Teoria dei codici |
| 3 | Costruzione di un gruppo non sofico | Teoria dei gruppi / algebre di operatori |
| 4 | Un controesempio alla congettura di rigidità di Connes | Algebre di operatori |
| 5 | Nuovi limiti inferiori per il calcolo della permanente | Complessità dei circuiti aritmetici |
| 6 | Ripetizione parallela esponenziale per giochi finiti arbitrari | Complessità quantistica |
| 7 | Hardness di approssimazione a fattore polinomiale per il Closest Vector Problem | Crittografia su reticoli |
| 8 | Il volume massimo esatto in ogni dimensione (Ehrhart) | Geometria discreta |
| 9 | Un limite inferiore super-esponenziale per i numeri di Ramsey multicolore | Combinatoria estremale |
| 10 | Controesempi alle congetture di compattezza e degenerazione | Teoria estremale dei numeri |
Perché matematica + TCS come superficie di rivelazione
Tre ragioni pratiche — nessuna misteriosa, una volta che le noti:
- Le affermazioni verificabili a macchina non si possono spinnare. Un numero di benchmark è un pixel di marketing; una dimostrazione Lean o type-checka o no. Questa è la dichiarazione di capacità più pulita possibile in un anno in cui le affermazioni di ogni laboratorio vengono messe in discussione.
- Nessuna accusa di gaming della leaderboard. Nessuno sospetta che Astra abbia memorizzato soluzioni di problemi precedentemente irrisolti.
- Ottiche regolatorie. OpenAI sta portando Astra attraverso il nuovo processo di revisione federale USA. "Il nostro nuovo modello ha fatto avanzare questioni aperte in crittografia e complessità quantistica" è una cornice molto diversa da "il nostro nuovo modello ha fatto 96% su SWE-Bench".
Cosa cambia oggi nella tua decisione Claude vs GPT-5.6
Niente che richieda azione questo mese. Astra non ha superficie di prodotto: non ci puoi costruire sopra. Il tuo tradeoff attivo è ancora quello di Scegliere un modello:
- Ingegneria software su repo reali, refactor grandi, loop di tool lunghi su una piattaforma ben gestita → Claude Opus 5 (
claude-opus-5) o Fable 5 (vedi Opus 5 field guide, Fable 5 / Mythos 5 flagship). - Lavoro long-context ad alto volume al tier più economico praticabile → GPT-5.6 Luna a $1 in / $6 out con l'intero contesto da 1,05M (Sol / Terra / Luna).
- Task browser-heavy o a forma di agent-index → GPT-5.6 Sol o Gemini 3.6 Flash (Famiglia Gemini 3.6 Flash).
- Ricerca o ingegneria multi-agente long-horizon — la forma esatta a cui punta Astra — la cosa più vicina disponibile oggi sono le native multi-agent API in beta sulla Responses API di OpenAI, e i managed agents + memory stores di Anthropic. Entrambi sono prodotti in commercio; Astra no.
Dovresti aspettare Astra?
- Astra non ha API, non ha prezzo e non ha una finestra di rilascio pubblicamente dichiarata. La divulgazione è un post di ricerca, non un annuncio di prodotto. Spedisci su quello che esiste; migra dopo, se il rapporto prezzo/qualità lo giustifica.
- La forma dichiarata di Astra — 'più agenti che coordinano compiti a lungo termine, per ore o giorni' — sarà un bersaglio in movimento. Tieni prompt, tool e orchestrazione dietro interfacce pulite (vedi porting dei prompt tra modelli), così potrai calare un nuovo provider senza riscrivere l'app.
- Le dieci dimostrazioni sono un segnale significativo per esattamente una classe di task: ragionamento matematico/formale rigoroso. Se è il tuo carico, iscriviti alla pagina di ricerca di OpenAI e rivaluta il giorno in cui si apre una preview o un'API.
- Non puoi comprare uno SLA su una divulgazione di ricerca. Le preview frontier slittano; la revisione regolatoria può aggiungere mesi. Torna a valutare quando ci saranno una pagina prezzi, una model card e un rate limit.
Verifica localmente le dieci dimostrazioni
# Requires elan (Lean toolchain manager) # Install: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh git clone https://github.com/openai/ten-proofs.git cd ten-proofs lake exe cache get # pre-built mathlib artifacts lake build All # type-checks every proof; exits 0 on success
Se lake build All esce con 0, ognuna delle dieci dimostrazioni type-checka contro mathlib. È la più forte affermazione di capacità che OpenAI abbia pubblicato quest'anno ed è verificabile sul tuo laptop.
Tre cose che i giornalisti continuano a sbagliare
Dove AILmanac aggiornerà questa pagina
Aggiorneremo lastVerified su questa pagina solo quando OpenAI pubblicherà una model card, un endpoint API, un tariffario o una nota ufficiale di rollout su ChatGPT — non su voci. Nel frattempo, le dieci dimostrazioni e la cornice multi-agente sono i fatti durevoli da ricordare.
- Quando ci sarà una pagina prezzi → questa pagina diventerà una scheda Astra completa con la tabella dei tier, nella stessa forma di Sol / Terra / Luna e di Opus 5.
- Quando ci sarà un'API → aggiungeremo una sezione "porta il tuo prompt Claude Opus 5 su Astra", accanto alla guida esistente porting dei prompt tra modelli.
- Se Anthropic pubblicherà una primitiva comparabile di 'multi-agente long-horizon' → aggiorneremo managed agents e faremo cross-link.
Check yourself
0/3Fonti e ulteriori letture
- Ten advances in mathematics and theoretical computer science — formalizzazioni Lean (
openai/ten-proofssu GitHub, Apache-2.0) — l'artefatto primario: dieci dimostrazioni Lean 4 che puoi type-checkare in locale. - OpenAI announces its "next major model" Astra by dropping ten previously unsolved math solutions (The Decoder) — il write-up tecnico più chiaro della divulgazione del 1 ago 2026.
- OpenAI smuggled the announcement of Astra into a blog post about math (Gizmodo) — la storia dell'ambiguità di naming (GPT-6 vs Astra vs variante GPT-5) e il reporting sulla demo di DC.
- OpenAI Astra: Next Major Model Explained (explainx.ai) — include la lista dei "non confermati" che quasi tutta la copertura di lancio ha saltato.
- Letture correlate su AILmanac: Scheda GPT-5.6 Sol / Terra / Luna • Opus 5 field guide • Native multi-agent APIs • Porting dei prompt tra modelli • Scegliere un modello.
Prossimi passi
- Modelli e prezzi correnti — la tabella prezzi live che AILmanac tiene ancorata alla documentazione ufficiale (Astra sarà aggiunto il giorno in cui avrà un prezzo ufficiale).
- Questo mese in Claude e AI — il digest rotante dove atterrano i nuovi fatti su Astra man mano che OpenAI li pubblica.
- Harness per agenti long-running — l'approfondimento frontier sulla forma di lavoro a cui punta Astra, dal lato Claude / Managed Agents.