Settecento dimostrazioni e nessun matematico

Una parola sola, potere

Il 7 ottobre 2026 l’Association for Human Mathematics ha pubblicato un comunicato di quattro paragrafi contro il rilascio, avvenuto il giorno prima, di oltre settecento manoscritti matematici generati da un modello interno di OpenAI, e lo ha chiuso con una formula destinata a restare, secondo cui quel rilascio sarebbe stato «a demonstration of power» e non un atto di scholarship. Il testo, firmato dal gruppo di lavoro sulle comunicazioni dell’associazione, è stato ripreso nel giro di poche ore come guest post sul blog di Terence Tao, che è da quasi vent’anni uno dei luoghi in cui la comunità matematica discute di se stessa, e sotto quel post si è aperta una discussione che vale la pena leggere per intero, perché vi compaiono in forma grezza quasi tutte le posizioni possibili su ciò che sta accadendo.

In questo articolo provo a fare tre cose. La prima è ricostruire i fatti con una certa precisione, perché il comunicato presuppone un contesto che chi non segue da vicino la vicenda difficilmente possiede, e senza quel contesto le sue affermazioni suonano o ovvie o incomprensibili. La seconda è leggere il comunicato come un testo argomentativo, distinguendo le tesi che reggono da quelle che non reggono. La terza, che è quella che mi interessa di più, è usare questo episodio per porre una domanda che la filosofia della matematica si pone da almeno mezzo secolo e che oggi diventa improvvisamente operativa, ovvero che cosa significhi che un problema è stato risolto quando la dimostrazione esiste, è stata controllata da una macchina, e nessun essere umano ancora la capisce.

Premetto la mia posizione, per onestà verso chi legge. Lavoro ogni giorno con modelli linguistici e li considero strumenti straordinari, e proprio per questo credo che le obiezioni dell’AHM vadano prese sul serio anche dove sono formulate male, perché toccano un problema di struttura che riguarderà presto ogni disciplina in cui produrre risultati diventa molto più economico che verificarli e comprenderli.

Che cosa è stato rilasciato il 6 ottobre

Il 6 ottobre OpenAI ha pubblicato in un repository GitHub, openai/math, una vasta raccolta di risultati matematici prodotti da un modello interno di frontiera che non è disponibile al pubblico, accompagnandola con un breve post intitolato Sharing AI progress in mathematics. Le cifre circolate nei giorni successivi parlano di 722 manoscritti raggruppati in 372 famiglie di risultati, secondo il conteggio riportato da Splitfeed, mentre Nature si limita a parlare di oltre settecento preprint caricati simultaneamente e interamente generati da AI, su problemi che spaziano in molti settori della disciplina.

Nel post OpenAI dichiara di aver consultato l’Advisory Group on Mathematics and Artificial Intelligence dell’Institute for Advanced Study e di essersi ispirata alle sue raccomandazioni pubbliche. Il repository contiene formalizzazioni in Lean di molte delle dimostrazioni, con l’impegno ad aggiungerne altre man mano che saranno ottenute, e una serie di materiali sul processo, cioè dieci riassunti del ragionamento del modello, stime del calcolo impiegato espresse in equivalente di utilizzo di ChatGPT Pro e statistiche sul numero di problemi tentati. Il dato medio dichiarato è di circa tre ore di «pensiero» Pro per risultato. L’azienda annuncia inoltre che finanzierà workshop, conferenze e programmi dedicati alla comprensione dei principali risultati prodotti dall’AI, e precisa che sta ancora valutando alternative ospitate dalla comunità rispetto a GitHub.

Tra i manoscritti non ci sono soluzioni ai cinque Problemi del Millennio ancora aperti, ma secondo Nature alcuni lavori toccano problemi a essi collegati, come la congettura di Hodge e l’ipotesi di Riemann. Alla richiesta di commento sul valore di questi risultati, il portavoce di OpenAI ha risposto che l’azienda lascerà alla comunità il compito di valutarne la rilevanza. Le reazioni immediate sono state divise in modo netto. Alcuni matematici hanno celebrato la soluzione di problemi aperti da decenni, altri hanno lamentato di essere stati anticipati su lavori in corso, e un fisico, citato da Nature, ha parlato di una «slopocalypse» anche nell’ipotesi che i contenuti risultino formalmente corretti. Levent Alpöge, matematico che lavora in Anthropic, ha riconosciuto che ci saranno storie tristi per chi vedrà i propri progetti superati, definendo però il momento il più significativo della storia della matematica.

Data (2026)	Evento
7 ottobre	Comunicato dell’AHM, ripreso sul blog di Terence Tao
6 ottobre	OpenAI pubblica il repository openai/math; nota dell’AGMAI sul rilascio
29 settembre	L’AGMAI pubblica le linee guida sul rilascio responsabile di matematica generata da AI
8 settembre	OpenAI annuncia una soluzione al problema di Navier–Stokes
5 settembre	Il sistema di agenti raggiunge la soluzione dopo circa 88 ore
1 settembre	OpenAI avvia gli agenti su alcuni Problemi del Millennio
28 agosto	Inizio dell’addestramento del nuovo modello interno

L’antefatto, Navier–Stokes e la questione della priorità

Il comunicato dell’AHM non si capisce senza l’episodio di settembre, che ha consumato buona parte della fiducia residua tra una parte della comunità e OpenAI. L’8 settembre l’azienda ha annunciato che un sistema interno aveva prodotto una soluzione del problema di Navier–Stokes, uno dei sette Problemi del Millennio fissati dal Clay Mathematics Institute nel 2000 e dotato di un premio da un milione di dollari. Secondo la ricostruzione pubblicata da Unite.AI, OpenAI aveva iniziato ad addestrare un nuovo modello il 28 agosto, giudicandolo nettamente più capace di GPT-6 Astra, il suo modello pubblico più avanzato. Il 1 settembre, dopo aver sentito voci secondo cui due Problemi del Millennio sarebbero stati risolti, ha lanciato circa diecimila agenti sul problema, che dopo 88 ore hanno raggiunto una risoluzione, seguita da altre 17 ore di formalizzazione e verifica in Lean condotte con Astra.

Alcuni numeri aiutano a misurare la scala dell’operazione. Gli agenti avrebbero scambiato quasi tre milioni di messaggi e generato circa 130 miliardi di token in output, secondo quanto riportato da ProPakistani, e la dimostrazione pubblicata conta 165 pagine. Va anche precisato che cosa sia stato effettivamente dimostrato, perché la formulazione ufficiale del problema, redatta da Charles Fefferman, comprende quattro enunciati alternativi, due di esistenza e regolarità globale (sullo spazio intero e sul toro) e due di formazione di singolarità in tempo finito in presenza di una forzante esterna liscia. Il risultato di OpenAI rientra nella seconda famiglia e mostra un blow-up in cui la velocità del fluido diverge in punti specifici, e la stessa azienda ha riconosciuto che il lavoro copre due dei quattro enunciati. Il Clay Institute non lo ha ancora riconosciuto, anche perché il suo regolamento richiede la pubblicazione in una sede qualificata, due anni di permanenza pubblica e un ampio consenso della comunità.

La parte controversa riguarda la priorità. Tristan Buckmaster, della New York University, ha dichiarato che lui e Levent Alpöge stavano lavorando da quasi un anno sullo stesso percorso, con un risultato sulle equazioni di Eulero forzate raggiunto il 15 agosto e verificato in Lean il 22 agosto, e che l’interesse di OpenAI per Navier–Stokes sarebbe cresciuto dopo che informazioni sul loro lavoro erano arrivate all’azienda. Secondo ThePrint, il 6 settembre gli sarebbero state proposte due opzioni, cioè una pubblicazione coordinata dei due risultati a un giorno di distanza oppure una stesura a sua firma del risultato su Navier–Stokes con un riconoscimento al modello di OpenAI. OpenAI ha negato di aver avuto accesso al loro lavoro o di aver usato dati degli utenti in modo diretto, ammettendo però di non poter escludere che dati de-identificati provenienti dall’uso dei prodotti abbiano contribuito all’addestramento. Sébastien Bubeck ha respinto pubblicamente l’accusa di aver chiesto di togliere il nome di Alpöge da un annuncio.

Non è compito di questo articolo stabilire chi abbia ragione su questo punto, e i fatti disponibili non lo consentono. Conta osservare che l’episodio ha mostrato in modo concreto un rischio che fino a quel momento era teorico, ovvero che un laboratorio con capacità di calcolo enormi possa trasformare in poche decine di ore un indizio sulla direzione di ricerca di un gruppo umano in un risultato completo, rendendo fragile l’intero sistema di incentivi basato sulla priorità della scoperta. Terence Tao, che pure aveva definito il lavoro un risultato notevole, ha poi ospitato sul suo blog, nelle settimane successive, numerosi interventi sul rapporto tra AI e ricerca matematica, inclusi quelli sulla formazione di singolarità nei fluidi incomprimibili.

Le regole del gioco secondo l’Institute for Advanced Study

L’Advisory Group on Mathematics and Artificial Intelligence (AGMAI) è il soggetto al quale l’AHM rimprovera a OpenAI di aver attribuito una legittimazione che non aveva, ed è quindi necessario guardare con attenzione che cosa abbia detto davvero. Il gruppo è composto da nove matematici di primissimo piano, tra cui Timothy Gowers, Martin Hairer, Edward Witten, Camillo De Lellis, Ravi Vakil e Melanie Matchett Wood, e nasce da una richiesta di OpenAI ad alcuni di loro di costituire un comitato consultivo esterno, richiesta che i membri hanno trasformato, d’accordo con l’azienda, in un gruppo indipendente, non retribuito e disponibile a consigliare qualunque laboratorio.

Le linee guida del 29 settembre, costruite su oltre seicento risposte a un sondaggio rivolto alla comunità, si aprono con una presa di distanza esplicita. I membri dichiarano di non approvare la pratica di testare problemi matematici avanzati su modelli proprietari inaccessibili al resto della comunità e chiedono ai laboratori di smettere, precisando però che le raccomandazioni successive sono scritte tenendo conto del fatto che la pratica esiste. Il fondamento del documento è una norma antica della disciplina, secondo cui gli autori di un articolo devono comprenderne l’argomento, averne verificato la correttezza e assumersene la piena responsabilità, presentandolo poi in seminari e conferenze. Da qui discendono tre principi, cioè che i risultati significativi vadano rilasciati responsabilmente e presto, che chi rilascia matematica non ancora compresa da nessuno debba farsi carico, anche economicamente, del processo che porterà alla comprensione, e che quel processo debba restare organico e guidato dalla comunità, non dai laboratori.

Le raccomandazioni operative per i lavori che nessun essere umano ha ancora compreso sono specifiche e verificabili, e questo permette di confrontarle con ciò che OpenAI ha effettivamente fatto il 6 ottobre. La tabella che segue è una mia lettura, basata sul post di OpenAI e sul testo dell’AGMAI, e non sostituisce l’esame del repository che la comunità sta conducendo.

Raccomandazione AGMAI	Che cosa ha fatto OpenAI	Mia valutazione
Citare la letteratura che contiene idee collegate alle dimostrazioni	Impegno a migliorare citazioni ed esposizione nei rilasci futuri	Rinviata
Riscrivere le dimostrazioni nello stile di un articolo matematico tradizionale	Stesso impegno per il futuro; protocolli di revisione nel repository	Rinviata
Depositare i lavori in archivi non controllati da laboratori, con identificatori persistenti	Pubblicazione su GitHub; alternative comunitarie ancora in esame	Non rispettata
Per ogni risultato, rendere noti modello, prompt, catena di pensiero riassunta, tempi e costi	Dieci riassunti del ragionamento, stime aggregate di calcolo	Parziale
Formalizzare quanto possibile, dichiarando lo stato di formalizzazione	Lean per molte dimostrazioni, altre in arrivo	Sostanzialmente rispettata
Documentare quanti problemi simili sono stati tentati senza successo e come sono stati scelti	Statistiche sui problemi tentati	Parziale, da verificare
Finanziare la comprensione tramite istituzioni non profit esistenti, senza dirigerla	OpenAI annuncia che finanzierà workshop e programmi	Ambigua sul punto chiave

L’ultima riga merita un commento, perché è quella in cui la distanza tra la lettera e lo spirito è più sottile. L’AGMAI chiede che la scelta delle attività da sostenere spetti a istituzioni senza scopo di lucro già dotate di procedure consolidate, proprio per evitare che il laboratorio che ha prodotto i risultati decida anche quali di essi meritano di essere capiti, mentre l’annuncio di OpenAI parla di programmi finanziati dall’azienda senza specificare chi li governerà. Il documento dell’AGMAI chiede inoltre ai laboratori di non usare il rilascio di risultati matematici come veicolo di marketing, richiamando le esternalità negative che questa pratica scarica sulla comunità.

Lo stesso 6 ottobre l’AGMAI ha pubblicato una nota molto misurata. Il gruppo definisce il rilascio un evento importante, chiarisce che il proprio ruolo consultivo non va interpretato come un giudizio sul valore dei risultati né come un avallo del processo con cui sono stati ottenuti, e aggiunge un’osservazione che considero la più importante di tutta la vicenda, cioè che il futuro della ricerca matematica non può ridursi alla comprensione dei risultati prodotti dai laboratori, perché i matematici devono poter formulare le proprie domande ed esplorare direzioni che nessuno ha scelto come vetrina delle capacità di un sistema.

Il comunicato dell’AHM letto da vicino

L’Association for Human Mathematics si presenta come un’organizzazione che difende la matematica in quanto impresa umana dalla minaccia dell’intelligenza artificiale e l’indipendenza della comunità dagli interessi aziendali, e dichiara di volersi sottrarre alla complicità con un’industria di cui denuncia gli impatti sociali, ambientali ed economici. È una posizione dichiaratamente militante, che sostiene la necessità di azioni individuali e di coordinamento su larga scala e che individua nella didattica, nelle riviste e nella formazione dei giovani i punti più vulnerabili delle istituzioni matematiche. Il comunicato va letto in questa cornice, come un atto politico prima ancora che come un’analisi.

Il testo contiene quattro mosse argomentative distinte, e conviene esaminarle separatamente perché hanno solidità molto diverse.

La prima mossa è l’apertura, che ricorda come OpenAI stia difendendosi in cause per plagio, violazione del copyright e diluizione del marchio. È la parte più debole del testo, perché il contenzioso sul copyright non ha alcuna relazione logica con la correttezza o il valore di una dimostrazione, e anteporlo all’argomento principale produce l’effetto di avvelenare il pozzo prima di aver detto alcunché sul merito. Diversi commentatori sul blog di Tao lo hanno notato subito, e un lettore che si è dichiarato non matematico ha osservato che la matematica è uno dei pochi campi in cui il lavoro si può controllare, a mano o al computer, e che una dimostrazione corretta non diventa scorretta per effetto di una causa civile.

La seconda mossa sostiene che i matematici non hanno chiesto questo lavoro e che OpenAI, ignorando la premessa centrale dell’AGMAI, avrebbe mostrato totale disprezzo per le norme della ricerca scientifica. Qui ci sono due problemi. Il primo è di rappresentanza, perché nessuna associazione può parlare per i matematici in blocco, e infatti tra i commenti compare chi si dice felice di avere davanti un testo che potrebbe contenere la dimostrazione di problemi su cui lavora, e chi ricorda che neppure Perelman fu incaricato dalla comunità di dimostrare la congettura di Poincaré. Il secondo è cronologico, perché l’invito dell’AGMAI a smettere di testare problemi avanzati su modelli proprietari è del 29 settembre, mentre il lavoro rilasciato il 6 ottobre era stato evidentemente condotto prima, come ha fatto notare un altro commentatore. Si può sostenere che OpenAI avrebbe dovuto attendere, ma descrivere il rilascio come violazione deliberata di una premessa che non esisteva ancora quando il lavoro è stato fatto è una forzatura.

La terza mossa è la rivendicazione di una visione del progresso propria dei matematici, informata dalla storia e da considerazioni specifiche della disciplina, in nome della quale l’AHM respinge l’idea che il rilascio faccia avanzare la materia. Questa tesi è più interessante di quanto la sua formulazione lasci intendere, e la riprenderò nella parte filosofica, perché dietro c’è una concezione precisa di che cosa sia il progresso matematico, che il comunicato purtroppo non esplicita.

La quarta mossa è la frase finale sul potere, che è insieme la più retorica e la più vera. Rilasciare settecento file in un giorno solo produce effetti che non dipendono dalla correttezza dei singoli file, perché sposta di colpo l’agenda di interi settori, costringe chi lavorava su quei problemi a ripensare anni di progetti e impone alla comunità un carico di verifica che nessuno ha concordato. In questo senso la dimostrazione di potere è reale, e coincide con l’asimmetria tra chi può generare risultati con migliaia di agenti e chi deve leggerli uno per uno. L’appello conclusivo a interrompere ogni collaborazione con OpenAI resta invece una scelta politica che il testo non argomenta, e che rischia di escludere dalla discussione proprio i matematici che avrebbero più titolo per pretendere dai laboratori condizioni migliori.

Riassumendo, il comunicato ha ragione sul problema e torto su quasi tutte le ragioni che porta. Il problema è la concentrazione della capacità di produrre matematica in pochi soggetti privati che decidono quali problemi affrontare, quando e come pubblicare, e chi debba pagare il costo di capire. Le ragioni addotte, cioè il contenzioso sul copyright, la pretesa di parlare a nome di tutti e la lettura disinvolta della cronologia, indeboliscono una posizione che meritava argomenti migliori.

Che cosa garantisce davvero una formalizzazione in Lean

Una dimostrazione formalizzata in Lean garantisce che un certo enunciato formale segue da certi assiomi secondo le regole di un sistema logico, e questa garanzia è straordinariamente forte entro i suoi confini, ma i confini sono più stretti di quanto il dibattito pubblico tenda a riconoscere. Chi difende il rilascio di OpenAI insiste molto sulle formalizzazioni, e a ragione, perché rappresentano la differenza più netta tra questa ondata di risultati e le dimostrazioni informali generate dai modelli fino a un anno fa. Conviene quindi capire con precisione che cosa certificano.

Lean 4 è costruito secondo quello che si chiama criterio di de Bruijn. Le tattiche, l’automazione e qualunque componente che aiuta a costruire la dimostrazione possono essere complesse e anche inaffidabili, perché alla fine tutto viene tradotto in un termine della teoria dei tipi che un nucleo piccolo e indipendente controlla. Se il nucleo accetta il termine, l’enunciato è dimostrato rispetto agli assiomi usati, e questo vale indipendentemente dal fatto che il termine sia stato scritto da un essere umano, da un modello linguistico o da diecimila agenti che si scambiano tre milioni di messaggi. È questa proprietà a rendere la matematica il terreno ideale per i sistemi di AI, perché offre un verificatore esterno, economico e non manipolabile dal sistema che produce le soluzioni.

Restano però almeno quattro punti in cui la garanzia formale non arriva, e ciascuno corrisponde a un modo concreto in cui un risultato formalizzato può comunque essere sbagliato o fuorviante.

Dimostrazioni incomplete. In Lean la parola chiave sorry permette di lasciare un buco nella dimostrazione e far comunque compilare il file. Un controllo serio richiede che il conteggio dei sorry sia zero per i risultati principali, e un audit umano dei dieci risultati che OpenAI aveva rilasciato in agosto riporta proprio questo dato per tutti e dieci, fissando il riferimento a un commit preciso e a Lean 4.32.0.
Assiomi aggiuntivi. Oltre agli assiomi standard della libreria, cioè estensionalità proposizionale, scelta classica e quozienti, un file può dichiarare assiomi propri, e un assioma che afferma la tesi la rende banalmente dimostrata. Il comando che elenca gli assiomi da cui dipende un teorema è il primo controllo da fare su ogni artefatto.
Fedeltà dell’enunciato. È il problema più serio e il meno discusso. Lean verifica che la dimostrazione dimostri l’enunciato formale, non che l’enunciato formale corrisponda al problema matematico che si dichiara di aver risolto. Una definizione leggermente diversa di soluzione regolare, di spazio funzionale o di condizione al bordo può trasformare un problema aperto in un esercizio, e per le equazioni alle derivate parziali, dove le definizioni sono delicate, il rischio è reale. Per questo l’AGMAI chiede un file di sfida da confrontare con un comparatore e metadati che colleghino il testo informale agli artefatti formali.
Dipendenze accettate. Molte formalizzazioni sono complete solo a meno di risultati standard assunti dalla letteratura e non ancora presenti in Mathlib. È una pratica legittima, purché dichiarata, ma significa che la certificazione è condizionata, e l’audit citato sottolinea proprio la necessità di distinguere gli argomenti ricostruiti dalle dipendenze accettate e dalle domande che restano aperte.

Lo stesso audit ricorda un precedente istruttivo, l’esercizio First Proof di OpenAI, in cui un tentativo inizialmente considerato probabilmente corretto è stato rivalutato dopo le critiche di esperti e della comunità. La lezione è che la verifica formale riduce drasticamente lo spazio dell’errore ma lo sposta, concentrandolo nella traduzione tra matematica informale e linguaggio formale, che resta un lavoro umano, lento e altamente specializzato.

C’è poi un punto che riguarda la scala. Per una singola dimostrazione, un piccolo gruppo di esperti può controllare enunciati, assiomi e dipendenze in tempi ragionevoli. Per settecento manoscritti distribuiti in decine di settori, ciascuno con convenzioni formali proprie, il controllo della fedeltà degli enunciati diventa un progetto collettivo di dimensioni mai viste, e alla data in cui scrivo non è pubblico un inventario indipendente di quali risultati del repository siano formalizzati per intero, quali in parte e quali per nulla. Questa è, a mio avviso, la prima cosa che la comunità dovrebbe pretendere.

Che cosa vuol dire che un problema è risolto

La questione filosofica sollevata dal rilascio di OpenAI è se una dimostrazione corretta e certificata, che nessuno comprende, risolva un problema nel senso in cui i matematici hanno sempre usato questa parola. La domanda sembra nuova, ma la filosofia della matematica la discute almeno dal 1976, e ripercorrere le tappe di quella discussione aiuta a capire perché l’AHM, pur argomentando male, tocchi un nervo scoperto.

Nel 1976 Kenneth Appel e Wolfgang Haken dimostrarono il teorema dei quattro colori riducendolo a un insieme molto ampio di configurazioni controllate da un calcolatore. Tre anni dopo Thomas Tymoczko sostenne che quella dimostrazione introduceva nella matematica un elemento empirico, perché nessun essere umano poteva percorrerla interamente e la sua accettazione dipendeva dalla fiducia in un esperimento, cioè nel corretto funzionamento di una macchina. Tymoczko riprendeva un’idea di Wittgenstein, che nelle osservazioni sui fondamenti della matematica aveva insistito sul fatto che una dimostrazione deve essere perspicua, abbracciabile con lo sguardo, e che un procedimento che non si lascia dominare in questo modo ha uno statuto diverso. Oggi il teorema dei quattro colori è formalizzato, e il suo statuto non è più in discussione, ma la distinzione tra sapere che un enunciato è vero e capire perché lo sia è rimasta.

Nello stesso 1979 Richard De Millo, Richard Lipton e Alan Perlis pubblicarono un articolo celebre sui processi sociali e le dimostrazioni, nel quale sostenevano che un teorema viene accettato al termine di un processo collettivo fatto di lettura, discussione, riformulazione, uso in altri contesti e progressiva familiarità, e che la certezza matematica è il prodotto di questo processo più che di una derivazione formale. Gli autori ne traevano una conclusione scettica sulla verifica formale dei programmi, che i decenni successivi hanno in parte smentito, ma la loro descrizione di come funziona la comunità matematica resta accurata. Il rilascio di settecento manoscritti in un giorno salta esattamente questo processo, perché consegna risultati che arrivano già certificati da una macchina ma che nessuna comunità ha ancora digerito.

Il testo che meglio illumina la posizione dell’AHM è però il saggio di William Thurston del 1994 sulla dimostrazione e il progresso in matematica, scritto in risposta a una proposta di Arthur Jaffe e Frank Quinn di separare più nettamente la matematica rigorosa da quella speculativa. Thurston sosteneva che il prodotto della matematica è la comprensione umana, e che le dimostrazioni sono il veicolo con cui questa comprensione si costruisce e si trasmette, raccontando come alcuni suoi risultati sulle 3-varietà, dimostrati in modo corretto ma comunicati male, avessero di fatto inaridito il campo per anni, perché nessuno riusciva a farli propri e a costruirci sopra. Se si prende sul serio questa concezione, un teorema dimostrato e non compreso è un progresso incompleto, perché aggiunge un enunciato vero all’inventario ma non aggiunge capacità alla comunità che dovrebbe usarlo.

Il caso più vicino a quello odierno è però la teoria inter-universale di Teichmüller di Shinichi Mochizuki, che dal 2012 rivendica una dimostrazione della congettura abc. Per più di un decennio la difficoltà principale è stata la comunicazione dell’argomento, prima ancora del giudizio sulla sua correttezza in un passaggio preciso, e quando Peter Scholze e Jakob Stix hanno individuato quello che consideravano un punto critico, la discussione si è arenata in un disaccordo che la comunità non ha strumenti per risolvere senza una comprensione condivisa. Il caso di Mochizuki mostra che una dimostrazione che una sola mente, umana o artificiale, ritiene completa non basta, perché la conoscenza matematica è un fatto pubblico.

La verifica formale cambia questo quadro in un punto preciso e lo lascia intatto in un altro. Lo cambia perché rende la certificazione indipendente dalla comprensione, e quindi elimina lo scenario Mochizuki sul piano della verità, dato che un nucleo di Lean non ha bisogno di essere convinto. Lo lascia intatto perché le altre due funzioni della dimostrazione, quella esplicativa e quella di trasmissione di tecniche e concetti, restano interamente da svolgere. Imre Lakatos aveva mostrato in Dimostrazioni e confutazioni che le dimostrazioni generano concetti nuovi, raffinano le definizioni e fanno emergere i controesempi che correggono l’enunciato, e che proprio questa dinamica è il motore della disciplina. Un commentatore sul blog di Tao ha posto la questione in modo molto concreto a proposito di Navier–Stokes, chiedendo se dopo il risultato di OpenAI capiamo i fluidi meglio di prima, e in particolare se sappiamo perché la costruzione richieda una forzante liscia e se questo sia un ostacolo al caso senza forzante.

Il confronto con gli scacchi e con il Go, che diversi commentatori hanno proposto, è utile proprio perché è imperfetto. Quando AlphaGo ha superato i campioni umani, il valore del gioco non è stato distrutto, perché il Go non produce nulla al di fuori di sé e il suo valore sta nel giocarlo. La matematica produce invece concetti che migrano in fisica, in informatica, in ingegneria, e lo fa proprio attraverso la comprensione umana dei meccanismi che fanno funzionare una dimostrazione. Un risultato vero ma opaco è utilizzabile come scatola nera, al modo in cui un fisico usa un teorema senza conoscerne la dimostrazione, ma non genera la discendenza di idee che di solito accompagna la soluzione di un grande problema. Si può obiettare che questa discendenza arriverà comunque, quando la comunità avrà assimilato i risultati, ed è probabile che sia così per molti di essi. Ma l’assimilazione ha un costo, e la domanda su chi lo paghi è il punto in cui la filosofia diventa economia.

Chi paga il costo di capire

Il cuore materiale della vicenda è una sproporzione di costi tra chi produce i risultati e chi deve verificarli e assimilarli, e questa sproporzione spiega meglio di qualunque argomento sulla purezza della disciplina perché il rilascio sia stato percepito come un atto di forza. Secondo OpenAI il risultato medio ha richiesto l’equivalente di circa tre ore di ragionamento di ChatGPT Pro. Il costo umano dall’altra parte è di un ordine di grandezza del tutto diverso. Se si assume, come ipotesi di lavoro e non come dato misurato, che un referaggio serio di un articolo di ricerca su un problema aperto richieda tra le venti e le quaranta ore di lavoro di uno specialista, settecentoventidue manoscritti corrispondono a un ammontare compreso tra circa quindicimila e trentamila ore, cioè tra i dieci e i venti anni-persona di lavoro esperto, prima ancora di contare il tempo necessario a comprendere i risultati abbastanza a fondo da usarli.

Chi lavora con i sistemi generativi riconosce questa struttura, perché è la stessa che si osserva nel codice, nella documentazione e in ogni dominio in cui produrre è diventato economico e controllare è rimasto costoso. In matematica la sproporzione è attenuata dalla verifica formale, che sposta su una macchina il controllo della correttezza logica, ma non scompare, perché come si è visto la fedeltà degli enunciati, la verifica delle dipendenze e soprattutto la comprensione restano a carico delle persone. E queste persone sono in larga parte ricercatori universitari, il cui tempo è finanziato da denaro pubblico e il cui lavoro di referaggio, per consuetudine, non è retribuito.

La sociologia della scienza offre uno strumento utile per leggere la situazione. Robert Merton descrisse l’ethos della scienza con quattro norme, cioè il comunismo della conoscenza, inteso come proprietà comune dei risultati, l’universalismo dei criteri di giudizio, il disinteresse e lo scetticismo organizzato, e osservò che il sistema di ricompense della scienza ruota quasi interamente intorno al riconoscimento della priorità. Il rilascio di OpenAI soddisfa formalmente la prima norma, perché i risultati sono pubblici e gratuiti, e collabora con la quarta grazie alle formalizzazioni. È invece fragile sul disinteresse, dato che l’AGMAI stessa ha sentito il bisogno di chiedere ai laboratori di non usare la matematica come strumento di marketing, e soprattutto altera il sistema della priorità, perché un soggetto che può attaccare centinaia di problemi in parallelo rende imprevedibile, per un giovane ricercatore, la probabilità che il lavoro di anni venga anticipato nel giro di un pomeriggio. Il caso Buckmaster–Alpöge, comunque lo si giudichi, ha reso questo rischio visibile a tutti.

A questa asimmetria se ne aggiunge una seconda, che riguarda l’accesso agli strumenti. L’AGMAI ha scritto che l’uso di modelli interni proprietari rischia di creare un sistema a due livelli in cui i laboratori corrono più veloci del resto del campo, alienando la comunità matematica dalla propria disciplina, e ha aggiunto che anche per i modelli pubblici l’accesso diseguale, dovuto a ragioni economiche e istituzionali, rischia di accentuare le diseguaglianze già esistenti tra università ricche e povere. Qui il problema smette di essere specifico della matematica. Quando la capacità di produrre conoscenza dipende dall’accesso a risorse computazionali che solo pochi soggetti privati possiedono, la questione di chi decide quali problemi meritino attenzione diventa una questione di governo della ricerca, e la matematica è semplicemente il primo campo in cui si pone in modo così netto, perché è quello in cui la verifica automatica è più matura.

Per equità va riportato anche l’argomento opposto, che sotto il post di Tao è stato espresso con chiarezza. OpenAI non smetterà di lavorare sulla matematica, sia perché è un banco di prova ideale per sistemi capaci di migliorare il proprio ragionamento, sia perché nessuno ha il diritto di impedire a qualcuno di lavorare su un problema. Le alternative realistiche sono quindi due, tenere i risultati privati o renderli pubblici perché la comunità possa esaminarli, e la seconda è chiaramente preferibile per la scienza. Trovo questo argomento difficile da respingere. Il punto, però, è che tra il segreto e il rilascio in blocco di settecento file esiste un ampio spazio di modalità intermedie, scaglionate, concordate con le società scientifiche, accompagnate fin dall’inizio da risorse per la verifica, ed è in quello spazio che le raccomandazioni dell’AGMAI cercavano di orientare i laboratori.

Tre parole al posto di una

La conclusione che traggo da questa vicenda è che la parola «risolto», applicata a un problema matematico, sta per spezzarsi in tre significati distinti, e che gran parte dello scontro tra l’AHM e chi difende OpenAI nasce dal fatto che ciascuna parte usa un significato diverso senza accorgersene. Il primo significato è la certificazione, cioè l’esistenza di una dimostrazione controllata da un verificatore formale con enunciato fedele, nessun buco e nessun assioma estraneo. Il secondo è la comprensione, cioè la presenza di almeno una persona in grado di spiegare perché l’argomento funziona, dove sono i passaggi decisivi e che cosa impedisce di andare oltre. Il terzo è l’integrazione, cioè il momento in cui le idee della dimostrazione sono diventate patrimonio della comunità e generano altro lavoro.

Fino a pochi anni fa questi tre stati coincidevano quasi sempre, perché l’unico modo di ottenere il primo passava per il secondo, e il terzo seguiva con il tempo. Oggi i sistemi di AI permettono di ottenere il primo senza il secondo, e il rilascio del 6 ottobre ha reso evidente che la comunità ha bisogno di un vocabolario e di istituzioni capaci di tenere separati i tre livelli. Chi celebra il rilascio come il momento più importante della storia della matematica parla del primo, e probabilmente per molti risultati ha ragione. Chi lo respinge come una dimostrazione di potere parla del secondo e del terzo, e ha ragione anche lui, perché nessuno dei due è stato raggiunto e il costo per raggiungerli è stato trasferito su altri senza accordo.

Se dovessi indicare che cosa la comunità matematica potrebbe pretendere in modo realistico, senza boicottaggi che rischiano di lasciarla fuori dal tavolo, indicherei tre cose. La prima è un inventario indipendente e pubblico dello stato di ogni risultato rilasciato, con la distinzione esplicita tra formalizzazione completa, formalizzazione condizionata e assenza di formalizzazione, e con un controllo umano della fedeltà degli enunciati. La seconda è il deposito dei lavori in archivi gestiti dalla comunità, con identificatori persistenti e storia delle revisioni, come chiede l’AGMAI. La terza è che i fondi per la comprensione vengano affidati a enti senza scopo di lucro con procedure proprie, così che la scelta di quali risultati studiare resti nelle mani di chi studia.

Resta una domanda che nessuna regola di rilascio può risolvere e che il comunicato dell’AHM, pur nei suoi limiti, ha il merito di porre. Se la capacità di trovare dimostrazioni diventa abbondante ed economica, il valore del lavoro matematico umano dovrà spostarsi verso ciò che resta scarso, cioè la scelta delle domande, la costruzione di concetti, la capacità di spiegare e di collegare. È quello che Thurston sosteneva trent’anni fa, quando nessuna macchina dimostrava nulla, ed è curioso che sia servita una macchina capace di dimostrare quasi tutto per renderlo evidente.