Ogni tanto arriva un annuncio che non c’entra niente con i listini e i prodotti, e che pure vale la pena capire bene, perché indica dove sarà il mercato tra due anni. Quello di OpenAI del 1° agosto è di questa specie: una versione interna di Astra ha chiuso dieci problemi matematici aperti. Proviamo a leggerlo senza fantascienza e senza cinismo, che sono i due modi standard di sbagliarlo.

Cosa è successo davvero

I fatti dichiarati. Una versione interna del prossimo modello di OpenAI ha risolto dieci problemi fino ad allora aperti in matematica e informatica teorica. Le soluzioni non sono testi persuasivi: sono dimostrazioni formali nel linguaggio Lean, pubblicate su GitHub, che un proof checker verifica meccanicamente. Tra i risultati, una costruzione che dimostra l’esistenza di gruppi non-sofici, questione centrale e aperta della teoria dei gruppi, e nuovi limiti per l’impacchettamento di sfere. Il costo di calcolo dichiarato per l’insieme dei risultati: circa 2.000 dollari. E il giudizio esterno più pesante possibile nel campo: Timothy Gowers, medaglia Fields, ha detto che raccomanderebbe una delle dimostrazioni per una rivista di prima fascia “senza esitazione”.

Perché stavolta il claim regge

Di annunci “l’AI fa scoperte” ne abbiamo letti tanti, e quasi tutti si sgonfiano alla verifica. Qui la struttura è diversa per una ragione tecnica: le dimostrazioni in Lean si verificano a macchina. Non serve fidarsi del comunicato, non serve un panel di esperti che rilegga: il correttore formale accetta o rifiuta, e chiunque può rieseguirlo. È il gold standard della verificabilità, e OpenAI ha scelto apposta il terreno dove il risultato non si può gonfiare.

Le domande legittime restano fuori dal perimetro della verifica: quanti tentativi falliti dietro i dieci successi, quanta selezione umana dei problemi, quanto il risultato generalizzi. Ma sono domande sul metodo, non sui teoremi: i teoremi sono veri.

Cosa c’entra con le aziende (la parte onesta)

Direttamente, poco: la teoria dei gruppi non compare in molti gestionali. Ma due trasferimenti sono concreti.

Il primo è il paradigma della verifica. La differenza tra questo annuncio e un benchmark è che l’output è meccanicamente controllabile. La stessa logica si applica ai domini aziendali dove esiste un verificatore: codice con suite di test, vincoli logistici con solver, configurazioni con validatori formali. La regola pratica che ne deriva: quando disegni un processo con AI, investi nel verificatore almeno quanto nel modello, perché l’AI che produce output verificabili vale il doppio di quella che produce output convincenti. È il principio che applichiamo da sempre nei progetti, e che qui trova la sua dimostrazione più elegante.

Il secondo è l’orizzonte del ragionamento lungo. Chiudere un problema aperto richiede catene di ragionamento che tengono per ore mantenendo coerenza formale: la stessa capacità che serve per audit complessi, ottimizzazioni di rete distributiva, verifiche di software critico. I modelli che sanno farlo in matematica lo porteranno in questi domini nel giro di pochi cicli di rilascio, e i primi ad accorgersene saranno i settori dove “dimostrabilmente corretto” vale più di “quasi sempre giusto”.

Cosa non è questo annuncio

Non è l’AGI, non è la fine dei matematici (la selezione dei problemi e l’interpretazione dei risultati restano lavoro umano di altissimo livello), e non è un prodotto: Astra non è disponibile, non ha listino, non ha data. È un segnale di traiettoria, del tipo più affidabile: verificato, costato poco, giudicato dai migliori del campo. I segnali di traiettoria vanno trattati come tali: si annotano nel piano a due anni, non nel budget del trimestre. Come sempre, chi vuole il quadro delle tendenze su cui vale la pena posizionarsi lo trova nel nostro report sui trend AI per le aziende italiane.

In sostanza: Astra ha dimostrato che la ricerca formale assistita da AI funziona e costa poco, e ha ricordato a tutti la regola che vale anche negli uffici: l’output verificabile batte l’output brillante. Se vuoi capire dove nel tuo processo manca un verificatore, parlaci del tuo progetto.

Domande frequenti

Secondo l'annuncio di OpenAI del 1° agosto, una versione interna del modello ha risolto dieci problemi fino ad allora aperti in matematica e informatica teorica, pubblicando su GitHub dimostrazioni formali verificabili a macchina nel linguaggio Lean. Tra i risultati: una costruzione che dimostra l'esistenza di gruppi non-sofici (una questione aperta centrale in teoria dei gruppi) e nuovi limiti per l'impacchettamento di sfere. Il costo di calcolo dichiarato: circa 2.000 dollari.

Le due cose insieme, ed è la parte interessante. Le dimostrazioni sono in Lean, quindi verificabili meccanicamente da chiunque: non serve fidarsi di OpenAI, il proof checker fa fede. E Timothy Gowers, medaglia Fields, ha detto che raccomanderebbe una delle dimostrazioni per una rivista di prima fascia senza esitazione. Restano domande legittime (quanti tentativi falliti dietro i dieci successi? quanto lavoro umano di selezione dei problemi?), ma i risultati in sé sono solidi nel modo più verificabile che la matematica conosca.

Perché sposta la questione dall'impresa al listino. Se risolvere un problema aperto costa l'ordine di grandezza di 200 dollari di GPU, la ricerca assistita da AI smette di essere un lusso da laboratorio nazionale e diventa una voce di budget accessibile a un'università media o all'R&D di un'azienda. È il pattern già visto altrove nell'AI: prima la dimostrazione che si può, poi il crollo del costo, poi la diffusione. L'annuncio dice che siamo alla seconda fase.

Direttamente, poco: pochi hanno problemi di teoria dei gruppi in produzione. Indirettamente, molto: la stessa capacità di ragionamento lungo e verificato che chiude un problema di matematica è quella che serve per verifiche formali di software critico, ottimizzazioni complesse di logistica o pricing e analisi dove la risposta deve essere dimostrabilmente corretta, non plausibile. Il punto operativo è il paradigma della verifica: l'AI che produce output controllabili meccanicamente vale il doppio di quella che produce output convincenti.