Un modello di OpenAI dichiara di aver risolto dieci problemi matematici irrisolti da decenni

OpenAI ha reso noto che una versione interna del suo modello di prossima generazione, chiamato Astra, ha prodotto dimostrazioni per dieci problemi aperti di matematica e informatica teorica. Le dimostrazioni sono state pubblicate in formato Lean, un linguaggio che permette la verifica automatica dei passaggi logici, e sono consultabili su GitHub.

Tra i risultati indicati dall’azienda figurano una costruzione che dimostrerebbe l’esistenza di gruppi non sofici, un oggetto di studio nella teoria dei gruppi, e nuovi limiti nel problema dell’impacchettamento delle sfere, una questione geometrica che occupa i matematici da secoli. Secondo quanto riferito da OpenAI, l’intero processo di calcolo necessario per arrivare a questi risultati sarebbe costato circa duemila dollari.

Il dato più discusso non è tanto la cifra economica quanto il rapporto tra costo e risultato: se confermati, problemi che hanno richiesto decenni di lavoro umano sarebbero stati affrontati con una spesa di calcolo relativamente modesta. È esattamente questo scarto a rendere l’annuncio rilevante, ma anche a richiedere cautela.

Il matematico Timothy Gowers, vincitore della medaglia Fields, ha commentato una delle dimostrazioni prodotte dal modello dicendo che la considererebbe pubblicabile «senza esitazione» su una rivista di primo livello. Si tratta di un giudizio autorevole ma isolato, riferito a una sola delle dieci dimostrazioni, e non equivale a una revisione paritaria completa dell’insieme dei risultati.

Astra, il modello che avrebbe prodotto questi risultati, non è stato ancora reso disponibile al pubblico. Le dimostrazioni pubblicate restano quindi nella fase in cui la comunità matematica può esaminarle liberamente, ma la verifica indipendente e sistematica — quella che stabilirebbe se i dieci problemi sono davvero risolti secondo gli standard della disciplina — non è ancora conclusa.

Va segnalato un limite di questa notizia: al momento proviene da un’unica origine, un comunicato della stessa OpenAI ripreso da una testata di settore; non esiste ancora una conferma indipendente della portata dei risultati né una revisione paritaria pubblicata. La disponibilità del codice e delle dimostrazioni su una piattaforma aperta permette in teoria un controllo esterno, ma la verifica di una dimostrazione formale in un ambito di ricerca avanzata richiede tempo, competenze specifiche e, di norma, la pubblicazione su riviste specializzate.

L’episodio si inserisce in un dibattito più ampio sul ruolo dei modelli linguistici nella ricerca matematica, un campo in cui la formalizzazione tramite linguaggi come Lean sta guadagnando terreno proprio perché permette di distinguere un’affermazione plausibile da una dimostrazione verificabile passo per passo. Per ora, i dieci problemi restano aperti nel senso pieno del termine: le prove esistono, sono pubbliche, ma la comunità scientifica non le ha ancora validate in modo definitivo.