Quando l’IA «risolve» una congettura senza dimostrazione: la risposta dei matematici

Immaginate che un modello di IA annunci di aver risolto una congettura geometrica vecchia di ottant’anni. Nessuna dimostrazione pubblicata su una rivista sottoposta a revisione tra pari, nessun codice sorgente disponibile, nessun dato di addestramento comunicato. Solo un comunicato stampa. Per un matematico, è più o meno convincente quanto un prestigiatore che sostiene di aver scoperto la legge di gravità perché fa levitare un cappello.

È proprio questo genere di situazione — raccontata da Ars Technica due settimane dopo un annuncio di OpenAI su un presunto risultato matematico — ad aver accelerato la stesura di un testo collettivo divenuto, nel giro di poche settimane, un evento per la comunità matematica internazionale. La Leiden Declaration on Artificial Intelligence and Mathematics, depositata il 2 giugno 2026 con DOI 10.5281/zenodo.20302944, non è un regolamento, né una legge, né un manifesto antitecnologico. È qualcosa di più raro: un testo normativo, redatto da ricercatori per ricercatori, proprio nel momento in cui una disciplina si accorge che le sue regole del gioco stanno cambiando senza essere stata consultata.

Tutto cominciò nel settembre 2025, durante un seminario al Lorentz Center di Leiden intitolato «Mechanization and Mathematical Research». Circa sessanta partecipanti provenienti da dieci paesi — matematici, informatici, storici e antropologi della scienza — si riunirono per discutere di ciò che l’automazione fa alla loro disciplina. Da questi scambi nacque un gruppo di lavoro convocato da Jim Portegies, della Eindhoven University of Technology, che trascorse i sei mesi successivi a elaborare un testo comune, come racconta l’Università di Leiden.

Il testo è firmato da sedici autori, con affiliazioni a Washington, Edimburgo, Amsterdam, Warwick, San Diego, Columbia, Cambridge, Oxford e Zurigo. Rodrigo Ochigame, storico e antropologo dell’IA alla Leiden University nonché coautore, riassume l’ambizione: «Abbiamo lavorato alla dichiarazione per diversi mesi, raccogliendo punti di vista differenti alla ricerca di principi condivisi.» Da allora il testo ha ricevuto il sostegno dell’International Mathematical Union, l’organizzazione internazionale associata, tra l’altro, alle medaglie Fields e al Congresso internazionale dei matematici (ICM). Il suo segretario generale, Christoph Sorger, ha voluto precisare: «L’IMU sostiene la Dichiarazione di Leiden perché costituisce un contributo tempestivo, serio ed equilibrato a un dibattito che è soltanto agli inizi.» E ha aggiunto: «Questo sostegno non significa la fine del dibattito.»

Il testo individua cinque valori fondamentali della ricerca matematica minacciati dall’uso attuale dell’IA: la certezza delle dimostrazioni, l’attribuzione verificabile dei risultati, la trasparenza degli argomenti, gli standard collettivi di valutazione e l’autonomia della disciplina dalle logiche commerciali esterne.

La prima minaccia è forse la più tecnica — e la più insidiosa. «Le attuali tecniche automatizzate possono produrre argomenti plausibili ma poco affidabili, se non addirittura errati, difficili da distinguere da vere dimostrazioni matematiche», avverte la dichiarazione. Il problema è chiaro: una dimostrazione matematica non è un testo che sembra una dimostrazione. È un oggetto logico di cui ogni passaggio deve poter essere verificato. Un grande modello linguistico può concatenare simboli con impressionante fluidità e al tempo stesso commettere un errore di ragionamento alla riga 47 — un errore che soltanto un esperto umano attento rileverà.

La distinzione è fondamentale. Come scrive Jeremy Avigad, professore alla Carnegie Mellon University, nel suo articolo sulla svolta formale in matematica: «Ora possiamo scrivere definizioni, teoremi e dimostrazioni in linguaggi idealizzati, simili ai linguaggi di programmazione, che i computer possono interpretare e verificare.» Ma verificare non significa generare. Ed è proprio qui che i modelli di IA generativa pongono un problema: generano senza offrire garanzie.

La seconda minaccia riguarda l’attribuzione e il diritto d’autore. Alcuni matematici vedono i propri articoli pubblicati su arXiv — liberamente accessibili, secondo la tradizione di apertura della disciplina — rastrellati per addestrare modelli commerciali, senza consenso né compenso. Ochigame lo dice senza mezzi termini: «Matematici che non avevano mai inteso contribuire allo sviluppo dell’IA vedono il proprio lavoro usato a questo scopo senza il loro accordo.»

La terza minaccia, più diffusa, è l’hype, il battage mediatico. Michael Harris, matematico alla Columbia University e coautore della dichiarazione, formula la diagnosi con precisione chirurgica: «L’industria tecnologica procede secondo una logica commerciale, antitetica ai valori della matematica.» Quando un’azienda annuncia un risultato matematico con un comunicato stampa prima di qualsiasi pubblicazione verificabile, aggira il processo di validazione collettiva che da secoli costituisce il cuore della pratica matematica.

Dietro le questioni etiche si cela una precisa domanda matematica e informatica. Come sapere che una dimostrazione è corretta se non possiamo verificarla noi stessi? La comunità degli assistenti alla dimostrazione formale — software come Lean o Coq — ha elaborato dagli anni Settanta una risposta elegante: il criterio di de Bruijn. Come spiegano Henk Barendregt e Freek Wiedijk nel loro articolo fondativo sulla sfida della matematica computazionale, un assistente alla dimostrazione soddisfa questo criterio se la dimostrazione prodotta può essere controllata indipendentemente da un piccolo programma di verifica, separato dal sistema che ha contribuito a costruirla. La fiducia non si fonda sull’intelligenza del generatore, ma sulla trasparenza del verificatore.

È proprio ciò che i modelli di IA proprietari non forniscono. Quando il modello è inaccessibile, come sottolinea Ochigame, «il modello di IA è proprietario e non è disponibile a nessuno esterno all’azienda», non è possibile applicare il criterio di de Bruijn. Nessuna verifica indipendente. Nessuna dimostrazione nel senso matematico del termine.

La biblioteca Mathlib, sviluppata per l’assistente alla dimostrazione Lean e descritta nell’articolo della comunità mathlib, illustra l’alternativa: un corpus comunitario di definizioni, teoremi e dimostrazioni verificate, che copre algebra, topologia, teoria delle categorie e analisi — costruito in modo distribuito, senza autorità centrale e liberamente consultabile. È il modello che la dichiarazione difende implicitamente: aperto, verificabile, attribuibile.

Le raccomandazioni sono precise e operative. I ricercatori sono invitati a dichiarare esplicitamente l’uso di strumenti automatizzati — grandi modelli linguistici, assistenti alla dimostrazione, software matematici — in una sezione dedicata dei loro articoli. La responsabilità dell’esattezza dei risultati resta umana. I risultati non devono essere presentati come prodotti esclusivamente da un’azienda o da un modello quando sono coinvolti contributi umani e lavori precedenti. E gli autori devono poter rifiutare che le loro pubblicazioni siano usate come dati di addestramento.

La dichiarazione non chiede di vietare l’IA in matematica. Leslie Ann Goldberg, responsabile dell’informatica all’University of Oxford e cofirmataria, formula con sobrietà il rischio reale: «Le bozze inesatte generate dall’IA sono economiche da produrre e si rischia di ingombrare la letteratura di presunti risultati che sono semplicemente falsi.» Il problema non è lo strumento. È l’assenza di norme per usarlo.

Peter Scholze, direttore del Max Planck Institute for Mathematics e medaglia Fields, riassume la posta in gioco filosofica: «Lo scopo della ricerca matematica è la comprensione umana della matematica; perciò la matematica può prosperare soltanto in una comunità di ricercatori umani.» La dichiarazione stessa lo esprime in una frase: «La matematica è, e deve sempre restare, un’impresa profondamente umana.»

Una discussione dedicata è prevista il 26 luglio 2026 durante l’ICM 2026, come annuncia l’IMU News del maggio 2026. Il dibattito è soltanto agli inizi.

Per comprendere con precisione la posta in gioco, occorre distinguere tre livelli nel rapporto tra IA e dimostrazione matematica.

Il primo livello è la generazione di testo matematico: un grande modello linguistico produce, in linguaggio naturale, un testo che sembra una dimostrazione. È ciò che fanno modelli come GPT-4 o Claude. Il problema è che plausibilità testuale e validità logica sono due cose diverse. Un modello può allucinare un passaggio di ragionamento con la stessa fluidità con cui enuncia un lemma corretto.

Il secondo livello è la verifica formale: una dimostrazione viene scritta in un linguaggio formale — Lean, Coq, Isabelle — che l’assistente alla dimostrazione può controllare meccanicamente. Come hanno mostrato Jeremy Avigad e John Harrison nel loro articolo pubblicato in Communications of the ACM, la verifica formale potrebbe diventare un nuovo standard di rigore in matematica. Qui la fiducia non si fonda sulla competenza del lettore, ma sulla logica del verificatore.

Il terzo livello, il più ambizioso, è l’autoformalizzazione: tradurre automaticamente una dimostrazione in linguaggio naturale in un oggetto formale verificabile. Il benchmark ProofNet, presentato in un articolo di Azerbayev, Piotrowski, Schoelkopf, Ayers, Radev e Avigad, contiene 371 esempi, ciascuno dei quali associa un enunciato formale in Lean 3, un enunciato in linguaggio naturale e una dimostrazione in linguaggio naturale, tratti da manuali universitari di analisi reale, algebra lineare e topologia. Risultato: nei loro esperimenti, il modello Code-davinci-002 formalizzava correttamente il 13,4% dei teoremi in modalità few-shot (ossia con alcuni esempi forniti nel contesto) e il 16,1% con il recupero di prompt simili. Il tasso di verifica sintattica (typecheck rate) raggiungeva il 45,2% con il recupero di prompt: ciò significa che più della metà degli output prodotti non superava neppure il controllo sintattico di Lean, prima ancora di qualsiasi questione di validità matematica.

Questi numeri non sono un atto d’accusa contro l’IA in matematica. Mostrano semplicemente che il cammino tra un «testo matematico convincente» e una «dimostrazione verificata formalmente» è ancora lungo — e che la Leiden Declaration fa bene a distinguere con cura le due cose.