L’ultima frattura segue la precedente affermazione di OpenAI di aver risolto il problema di Navier-Stokes, una sfida del Premio del Millennio. Quell’annuncio ha suscitato accuse secondo cui l’azienda avesse preceduto le norme accademiche e potesse aver beneficiato del lavoro in corso dei ricercatori, un’accusa che OpenAI ha negato. L’episodio ha lasciato diffidente un settore costruito su un esame lento e rigoroso nei confronti di un outsider ben finanziato che si muove alla velocità della Silicon Valley.¹

A settembre, il neocostituito Advisory Group on Mathematics and Artificial Intelligence (AGMAI) ha invitato i laboratori di IA a pubblicare tempestivamente i risultati attraverso canali consolidati, a rendere noti modelli, prompt e costi computazionali, e a evitare di trasformare le pubblicazioni di ricerca in marketing. Il suo monito era netto: le aziende dovrebbero «astenersi dal trattare la pubblicazione di risultati matematici come veicoli di marketing».²

Poi, martedì, OpenAI ha pubblicato 722 manoscritti che coprono 372 famiglie di risultati, affermando che un modello frontier interno aveva prodotto il lavoro. L’azienda ha detto di essersi ispirata ai consigli di AGMAI; il presidente di OpenAI Greg Brockman ha presentato l’iniziativa come un passo «verso l’accelerazione della scoperta scientifica e il miglioramento della qualità della vita per tutti».Greg Brockman (gdb)³

La portata ha impressionato perfino gli scettici. Un resoconto della pubblicazione ha affermato che dimostrava come i progressi dell’IA siano destinati a estendersi a nuovi campi specialistici, proprio come hanno già fatto gli strumenti di programmazione. Eppure Stephen Wolfram ha offerto il contrappeso: «Si possono produrre facilmente un trilione di teoremi. Il problema è che la maggior parte di quei teoremi non sarà qualcosa a cui qualcuno terrà».⁴

La verifica è ora il banco di prova immediato. Entro giovedì, OpenAI aveva ritirato le soluzioni ad almeno tre problemi dopo l’emergere di apparenti errori, mentre solo alcune dimostrazioni erano state formalizzate per il controllo automatico.¹ I critici sostengono che la pubblicazione resti al di sotto dello standard di AGMAI di garantire la comprensione umana: solo 10 dei 719 manoscritti includevano il ragionamento del modello e, secondo quanto riportato, il 42% non era stato sottoposto a formalizzazione.⁵

Per i sostenitori, la dimostrazione formale automatizzata potrebbe liberare i matematici affinché perseguano nuovi concetti. Per i critici, il lavoro difficile inizia dopo l’arrivo della risposta del modello: trasformare una dimostrazione dichiarata in conoscenza di cui la disciplina nel suo complesso possa fidarsi, che possa insegnare e sviluppare.