OpenAI ha pubblicato le soluzioni a oltre 370 problemi matematici rimasti aperti per decenni, generati da un modello interno non ancora disponibile al pubblico. Tra i risultati dichiarati c’è una dimostrazione formale del problema di Navier-Stokes, uno dei sette Problemi del Millennio del Clay Mathematics Institute. La comunità matematica non ha festeggiato.
Il modello ha iniziato il suo addestramento il 28 agosto e ha prodotto risultati a ritmo serrato: in media circa tre ore di calcolo per ciascuna soluzione. OpenAI sostiene che i risultati coprono la maggior parte delle aree della matematica. La portata della pubblicazione — centinaia di soluzioni rilasciate in blocco — ha però sollevato obiezioni immediate. Il gruppo consultivo formato dalla stessa azienda ha definito questa scelta “non una dimostrazione di rigore accademico, ma una dimostrazione di potere.”
A settembre, dopo le prime polemiche seguite alla pubblicazione della soluzione di Navier-Stokes, OpenAI aveva annunciato la creazione di un Advisory Group on Mathematics and Artificial Intelligence, ospitato presso l’Institute for Advanced Study di Princeton. Il gruppo è composto da nove matematici di primo piano, tra cui Timothy Gowers, Edward Witten e Martin Hairer. Tre di loro avevano già firmato la lettera aperta di protesta. Il gruppo opera in modo indipendente: i membri non ricevono compensi da OpenAI e possono rendere pubbliche le proprie posizioni senza filtri.
I limiti del mandato sono però espliciti. Il gruppo non ha potere di veto sulla ricerca interna né può rallentare i tempi di pubblicazione. OpenAI ha chiarito che il gruppo “non è responsabile di consigliare il ritmo dei progressi interni in matematica.” L’Institute for Advanced Study ha aggiunto che i suoi esperti non hanno “potere decisionale in alcuna azienda.” Venticinque vincitori della Medaglia Fields avevano già firmato una lettera aperta intitolata “A Severe Misalignment of AI in Mathematics”, denunciando il rischio che i laboratori di intelligenza artificiale stiano usando i risultati matematici come vetrina competitiva, aggirando il processo di revisione scientifica.
Le critiche tecniche sono concrete. Un recente articolo accademico ha evidenziato discrepanze tra le spiegazioni in linguaggio naturale prodotte dal modello e il codice formale in Lean allegato come verifica. Il problema non è solo stilistico: se la dimostrazione in linguaggio naturale e il codice formale non coincidono, non è chiaro cosa sia stato effettivamente dimostrato. C’è poi la questione del plagio: dato il volume delle soluzioni rilasciate simultaneamente, alcuni ricercatori sostengono che non sia stato condotto alcun controllo adeguato per escludere che il modello abbia riprodotto lavori preesistenti.
Il nodo di fondo è strutturale. La matematica è una delle poche discipline in cui un risultato può essere verificato meccanicamente — ed è questa la ragione per cui OpenAI ha scelto proprio questo campo come banco di prova. Ma la verifica formale non sostituisce la comprensione umana, e la comunità accademica chiede che le dimostrazioni siano accompagnate da una spiegazione intellegibile agli esperti del settore. Se nei prossimi mesi il processo di revisione darà esito positivo anche solo per una parte delle soluzioni pubblicate, il dibattito sugli standard cambierà tono. Se invece le discrepanze segnalate si moltiplicassero, l’intera operazione rischia di diventare un caso di studio su cosa succede quando la velocità supera il rigore.
