Ci hanno propinato una narrazione rassicurante, quasi domestica: modelli capaci di scrivere email, generare immagini o assistere gli sviluppatori. Sabato, invece, OpenAI ha mostrato qualcosa di radicalmente diverso. Una versione interna del modello Astra ha contribuito alla soluzione di dieci problemi matematici aperti da almeno un decennio e, in diversi casi, rimasti irrisolti per molte decine di anni. Se questi risultati continueranno a essere confermati dalla comunità scientifica, il settore potrebbe aver superato una soglia storica: l’intelligenza artificiale non si limiterebbe più ad assistere gli scienziati, ma inizierebbe a produrre nuova conoscenza.
La portata delle dimostrazioni è notevole. Tra i risultati annunciati figura la dimostrazione dell’esistenza di gruppi non sociali, una questione fondamentale della teoria dei gruppi, oltre a una confutazione della celebre congettura di rigidità di Connes, considerata uno dei riferimenti della moderna teoria degli operatori. Ancora più simbolico è il fatto che tre dei problemi risolti appartengano alla lunga lista di quesiti lasciati da Paul Erdős, identificati con i numeri 183, 146 e 180. Chi conosce la matematica sa che questi problemi non erano rimasti aperti per mancanza di interesse, ma perché avevano resistito ai migliori ricercatori del mondo.
L’aspetto forse più sorprendente riguarda il processo. Gli articoli scientifici sono stati redatti da matematici umani, ma il modello Astra ha formalizzato integralmente le dimostrazioni utilizzando Lean, uno dei più avanzati proof assistant esistenti. Questo significa che ogni singolo passaggio logico è stato verificato automaticamente da un computer, eliminando il rischio di errori nascosti che talvolta emergono anni dopo la pubblicazione di una dimostrazione. OpenAI ha inoltre pubblicato su GitHub i certificati di verifica, introducendo un livello di trasparenza raro persino nella ricerca accademica.
Questo dettaglio è meno spettacolare del titolo, ma probabilmente ancora più importante. La matematica moderna sta vivendo una trasformazione profonda grazie alla cosiddetta formal verification. Non basta più convincere i revisori di una rivista: una dimostrazione può essere certificata da un sistema che controlla rigorosamente ogni inferenza logica. L’intelligenza artificiale diventa così non soltanto uno strumento creativo, ma anche un garante della correttezza scientifica.
Colpisce anche il dato economico. Secondo OpenAI, il numero di token necessari per ottenere tutte e dieci le dimostrazioni corrisponderebbe a un costo di circa 2.000 dollari utilizzando le tariffe API di Sol. È una cifra irrisoria rispetto ai milioni di dollari investiti ogni anno in ricerca matematica avanzata. Naturalmente il costo dell’inferenza non racconta quello dell’addestramento del modello, che rimane enorme, ma offre una prospettiva interessante: una volta costruita l’infrastruttura, produrre nuova conoscenza potrebbe diventare sorprendentemente economico.
La vera implicazione strategica, tuttavia, va oltre la matematica. Se un modello riesce a individuare strutture e dimostrazioni che sfuggono agli esseri umani, nulla impedisce di immaginare applicazioni analoghe nella fisica teorica, nella chimica computazionale, nella progettazione di nuovi materiali, nella biologia molecolare o nella scoperta di farmaci. La matematica rappresenta il terreno ideale perché le dimostrazioni possono essere verificate formalmente, ma costituisce anche un laboratorio per comprendere come l’AI possa affrontare problemi scientifici di estrema complessità.
Negli ultimi mesi abbiamo assistito a una rapida evoluzione dei modelli di frontiera. DeepSeek ha migliorato le prestazioni degli agenti mantenendo dimensioni simili, Alibaba ha mostrato sistemi capaci di sviluppare software autonomamente per giorni consecutivi, Moonshot AI ha reso disponibile un gigantesco modello open weight con oltre cento miliardi di parametri attivi per inferenza. Ora OpenAI sembra voler spostare la competizione su un livello ancora più elevato: non chi genera meglio il codice o il testo, ma chi accelera direttamente il progresso scientifico.
Naturalmente è prematuro sostenere che l’intelligenza artificiale sostituirà i matematici. Le idee, la formulazione dei problemi e l’intuizione restano profondamente umane. Tuttavia la relazione tra ricercatore e macchina sta cambiando rapidamente. L’AI non è più soltanto un assistente che suggerisce una dimostrazione o completa un calcolo; diventa un collaboratore capace di esplorare spazi matematici che nessun individuo potrebbe percorrere da solo.
La Silicon Valley ha spesso venduto promesse che hanno impiegato anni per concretizzarsi. Questa volta, però, il valore non si misura nel numero di utenti o nella capitalizzazione di mercato, bensì nella capacità di produrre risultati verificabili che entrano nella letteratura scientifica. È una differenza sostanziale. Quando un algoritmo contribuisce a risolvere un problema aperto da decenni, l’hype lascia spazio ai fatti.
Forse il cambiamento più profondo è culturale. Per secoli abbiamo considerato la scoperta scientifica come l’espressione più alta dell’ingegno umano. Se sistemi come Astra inizieranno a contribuire regolarmente alla soluzione dei grandi problemi della matematica e delle scienze, entreremo in un’epoca nella quale le innovazioni più importanti nasceranno dalla collaborazione tra intelligenza umana e intelligenza artificiale. Non sarà la fine della ricerca tradizionale; sarà probabilmente l’inizio di una nuova rivoluzione scientifica, nella quale il vantaggio competitivo delle nazioni e delle aziende dipenderà sempre meno dal numero di ricercatori e sempre più dalla qualità dei modelli con cui quei ricercatori lavoreranno.
Ten advances in mathematics and theoretical computer science