La matematica è uno dei terreni più difficili per l’intelligenza artificiale. Non basta eseguire calcoli, la ricerca richiede di inventare strategie, collegare idee lontane e costruire dimostrazioni solide. È proprio su questo terreno che OpenAI ha deciso di alzare l’asticella. Il 6 ottobre la società ha pubblicato 722 manoscritti matematici, organizzati in 372 famiglie di risultati, prodotti da un modello frontier interno non ancora disponibile al pubblico. Il materiale, raccolto in un repository GitHub, riguarda problemi aperti in diverse aree. Il modello è stato sottoposto a circa 4.000 problemi. Non significa però che tutti siano stati risolti o accettati dalla comunità scientifica. OpenAI avverte che alcuni lavori non ancora formalizzati potrebbero contenere errori.
Uno degli aspetti più interessanti è il tentativo di rendere le dimostrazioni controllabili dalle macchine. Per molti risultati OpenAI ha preparato una formalizzazione in Lean, un sistema che permette di tradurre una dimostrazione in una forma verificabile da un computer. È diverso da una normale risposta generata da un chatbot, che può apparire convincente pur contenendo un errore logico. La verifica formale offre un controllo più rigoroso, ma non stabilisce da sola l’importanza di una scoperta. Non tutti i manoscritti hanno ancora una formalizzazione Lean. OpenAI continuerà ad aggiungerle e ha pubblicato anche dati sul processo: ogni risultato ha richiesto in media una quantità di calcolo equivalente a circa tre ore di “thinking” di ChatGPT Pro.
Il salto rispetto ai tradizionali test di matematica è soprattutto qualitativo. OpenAI sostiene che il modello possa esplorare questioni alle quali gli esseri umani non hanno ancora dato una risposta. L’iniziativa arriva dopo la soluzione generata dall’AI al problema delle equazioni di Navier-Stokes, uno dei sette Millennium Prize Problems. Anche quel risultato deve essere esaminato dalla comunità matematica.
Ed è proprio qui che emerge la questione più delicata. Una dimostrazione verificabile non equivale automaticamente a una scoperta già compresa dalla comunità. Un risultato può essere formalmente corretto e restare difficile da interpretare, collegare alla letteratura precedente o trasformare in una nuova linea di ricerca. L’Advisory Group on Mathematics and Artificial Intelligence, gruppo indipendente, ha definito la pubblicazione un evento importante, ma ha chiarito che si tratta dell’inizio, non della conclusione, del processo di comprensione. Il gruppo ha sottolineato che il futuro della matematica non può consistere soltanto nel comprendere risultati prodotti dai laboratori AI: i matematici devono continuare a formulare le proprie domande e sviluppare direzioni di ricerca autonome.
La questione riguarda anche il modo in cui la scienza potrebbe cambiare. Se un modello riesce a mantenere ragionamenti lunghi e produrre dimostrazioni controllabili, la matematica può diventare un banco di prova per capacità utili altrove. OpenAI indica biologia, fisica, scienza dei materiali, ingegneria e medicina come possibili aree di applicazione. Ma nelle scienze sperimentali contano anche dati e replicabilità. La domanda non è quindi se l’AI possa sostituire i matematici, ma quanto possa accelerarne il lavoro.
La pubblicazione mostra un possibile cambio di scala nella ricerca assistita dall’AI. Il modello è stato messo davanti a migliaia di domande aperte, lasciando agli esseri umani il compito di controllare e interpretare le soluzioni. È ancora presto per parlare di una rivoluzione: il materiale deve essere studiato. Ma se una parte significativa delle dimostrazioni dovesse resistere all’esame degli esperti, l’AI potrebbe passare dall’essere soprattutto uno strumento per usare la conoscenza esistente a diventare uno strumento per ampliarla.
OpenAI avrebbe risolto uno dei problemi del millennio usando migliaia di agenti AI
Ma due matematici accusano l'azienda di plagio. E uno lavora…
