OpenAI Astra: dieci problemi risolti, ma chi ha citato chi?

Fermati un secondo su un numero: duemila dollari. È quanto è costato, ai prezzi API pubblicati da OpenAI, risolvere dieci problemi di matematica rimasti aperti per decenni. Alcuni fermi da prima che nascessi, probabilmente. Tre vengono dal catalogo di Paul Erdős, il matematico morto nel 1996: sono rimasti senza risposta da prima ancora della sua morte. Il 1° agosto 2026 OpenAI ha messo tutto questo su GitHub, gratis, sotto licenza aperta.

Gli annunci del genere di solito vanno presi con le pinze, ma qui non devi credere a nessuno sulla parola. Ogni dimostrazione, 249 pagine in tutto, è stata scritta in Lean 4, un linguaggio che non lascia zone grigie: o il compilatore accetta la prova riga per riga, o la respinge. Il conteggio dei “sorry”, i segnaposto che in Lean indicano un passaggio non dimostrato, è zero su tutti e dieci i risultati. Il verificatore è pubblico. Chiunque può scaricarlo, farlo girare, e vedere con i propri occhi se il compilatore dice sì o no.

La reazione di Thomas Bloom, che gestisce il catalogo dei problemi di Erdős, è stata netta: l'ha chiamata “big news”, una grande notizia. Più importante, secondo lui, di un altro risultato dello stesso laboratorio, a maggio: la confutazione della congettura di Erdős sulle distanze unitarie. Quel risultato, per capirci, aveva convinto Timothy Gowers, medaglia Fields, che se lo avesse presentato un ricercatore umano agli Annals of Mathematics lo avrebbe raccomandato “senza alcuna esitazione”.

Tra i dieci risultati: la prima costruzione esplicita di un gruppo non sofico, una domanda rimasta aperta dal 1999; la confutazione di una congettura di Alain Connes sulle algebre di operatori; e, tra i tre di Erdős, il numero 183 sui numeri di Ramsey multicolore. Otto campi della matematica e dell'informatica teorica, toccati in un colpo solo, da un modello che al pubblico non è nemmeno ancora arrivato.

A questo punto l'articolo dovrebbe finire qui, con te convinto che la matematica sia appena cambiata per sempre. Invece c'è un'altra metà di questa storia, ed è quella che vale la pena leggere fino in fondo.

Francesco Fournier-Facio, teorico dei gruppi all'Università di Cambridge, è andato a fondo sul risultato più celebrato dei dieci — quello sui gruppi non sofici — e ha mostrato che la dimostrazione poggia in modo cruciale su lavori già pubblicati, quelli di Kun del 2016 e di Kun e Thom del 2019. Nel suo paper scrive che la novità sta più nell'enunciato che nella prova, e che esperti a conoscenza di quei lavori “probabilmente” avrebbero potuto dimostrarla da soli, ma forse non avrebbero pensato a formulare quell'enunciato. Due giorni dopo l'annuncio di Astra, il 3 agosto 2026, ha pubblicato su arXiv “A torsion-free non-sofic group”: non la stessa costruzione, ma una diversa fonte di esempi, basata sullo stesso criterio tecnico, che include anche gruppi senza torsione. L'ha firmato con il proprio nome, ed è verificabile da chiunque.

Ed ecco il punto logico: Lean verifica che i passaggi di una dimostrazione siano corretti. Non verifica se un'idea è nuova, se qualcuno l'aveva già avuta prima, o se il lavoro altrui è stato citato come si deve. Un compilatore può dirti con certezza matematica assoluta che una prova regge — e allo stesso tempo essere completamente cieco al fatto che una parte cruciale di quella prova poggia su articoli del 2016 e del 2019. La correttezza logica e la corretta attribuzione delle idee sono due assi completamente diversi, e un annuncio che mette in vetrina soprattutto il primo racconta la storia a metà.

Il 2 giugno 2026 è nata la Dichiarazione di Leiden, con l'endorsement dell'International Mathematical Union e oggi più di 4.000 firmatari. Mette in guardia dalle aziende IA che usano ricerca pubblicata senza consenso, aggirano la revisione paritaria e minacciano l'integrità della dimostrazione e dell'attribuzione. Su un punto l'annuncio di Astra ci finisce dentro: un comunicato aziendale, le prove su GitHub, e la revisione paritaria ancora da fare.

Uno dei dieci risultati, va detto, riguarda il Closest Vector Problem, uno dei nodi centrali della crittografia reticolare, la base matematica della crittografia post-quantistica che il mondo sta adottando proprio ora. Secondo le fonti, Astra ne ha rafforzato le stime di difficoltà, ed è una buona notizia. Ma dopo aver visto che almeno uno degli altri nove poggia in modo cruciale su lavori altrui, è legittimo chiedersi quanto fidarsi ciecamente anche di quello che non si è potuto controllare da soli.

Per anni la sicurezza informatica ha dato per scontato che certi problemi matematici fossero troppo duri da risolvere, punto e basta, per chiunque — umano o macchina. La stessa capacità di Astra, con lo stesso costo, potrebbe in teoria essere puntata a cercare debolezze invece che a confermare solidità. Quanto di tutto questo è vera scoperta, e quanto è una macchina PR che sa esattamente quale numero mettere in un titolo, è una domanda che, questa volta, nessun compilatore può risolvere al posto tuo.

Vi lascio spunti di riflessione - il futuro tecnologico busserà alle porte di molti, se non di tutti - dobbiamo capire come farlo entrare senza che diventi quello che domina completamente la nostra esistenza - dobbiamo proteggere ciò che crea l'umano per preservare la propria storia… cosa siamo realmente. Se le macchine iniziano a prendersi ciò che è nostro senza che noi ce ne accorgiamo potrebbe essere veramente la fine.

Ne abbiamo già parlato: Matrix ed Elysium non erano film, erano un avviso. E la batteria umana, oggi, è un telefono in mano.

Se hai bisogno per la tua azienda contattaci.

Fonti:
OpenAI's Astra Solved Decades-Old Math Problems For $2,000 — Forbes
OpenAI's Astra solves 10 long-open math problems and publishes the proofs — SiliconANGLE
OpenAI says its next model, Astra, has solved ten open problems in mathematics — The Next Web
OpenAI says next-generation model solved 10 major open problems in quantum complexity, mathematics — The Quantum Insider
OpenAI's Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs — Tech Times
openai/ten-proofs — repository GitHub con i certificati Lean 4 (Apache-2.0)
Ten advances in mathematics and theoretical computer science — OpenAI
A Human Audit of OpenAI's AI-Generated Mathematical Proofs — Sienicki e Sienicki (arXiv)
An AI solution to an 80-year-old problem has shocked mathematicians — The Conversation
Francesco Fournier-Facio – A torsion-free non-sofic group (arXiv, 3 agosto 2026)
Leiden Declaration on Artificial Intelligence and Mathematics