Nell’estate del 2025, diversi modelli di intelligenza artificiale hanno risolto cinque problemi su sei alle Olimpiadi Internazionali di Matematica, la competizione annuale riservata ai migliori studenti liceali del mondo. Pochi mesi dopo, a febbraio 2026, una sfida chiamata First Proof ha dato ai sistemi AI una settimana per risolvere dieci problemi di livello universitario scelti da matematici professionisti e che non apparissero nei dati di training. Più della metà dei problemi è stata risolta. Come ha scritto il matematico Daniel Litt in un post di analisi dei risultati: «È molto probabile che questa tecnologia sia più grande del computer».
Siamo di fronte a una svolta profonda. E pone una domanda che la filosofia della matematica non ha ancora saputo rispondere: se una macchina dimostra un teorema che nessun essere umano riesce a comprendere, stiamo ancora facendo matematica?
AlphaEvolve e la scoperta assistita
Il caso più emblematico del nuovo corso è AlphaEvolve, un sistema sviluppato congiuntamente da matematici — tra cui il medaglia Fields Terence Tao — e da Google DeepMind. Il funzionamento è semplice nella concezione, rivoluzionario nei risultati: Gemini scrive programmi Python che vengono poi “evoluti” attraverso algoritmi genetici per trovare soluzioni ottimali a problemi matematici aperti. Tra gennaio e maggio 2025 il team ha testato il sistema su 67 problemi in diverse aree della matematica. In 23 casi AlphaEvolve ha migliorato le migliori soluzioni note; in 36 ha eguagliato i risultati esistenti.
Un dettaglio degno di nota è emerso nell’interazione con il sistema. Come ha raccontato Javier Gómez-Serrano, matematico della Brown University, il modello rispondeva meglio ai prompt che contenevano incoraggiamento esplicito: frasi come «you can do this» sembravano migliorare le prestazioni. Non è chiaro perché, e questo è un primo segnale di un problema più ampio: l’intelligenza artificiale in matematica funziona, ma spesso non sappiamo esattamente perché.
La verifica formale e il paradosso della comprensione
Accanto alla scoperta automatica di nuovi risultati, un altro fronte si sta muovendo rapidamente: la verifica formale delle dimostrazioni. Strumenti come Lean, Isabelle, Rocq e F* esistono da decenni. Permettono di scrivere una specifica formale di ciò che un programma dovrebbe fare, e poi di dimostrare matematicamente che il codice soddisfa sempre quella specifica — inclusi i casi limite che nessun testatore umano avrebbe immaginato. Il problema è sempre stato il costo: per il microkernel seL4, ad esempio, 8.700 righe di codice C hanno richiesto 200.000 righe di dimostrazioni Isabelle e venti anni-persona di lavoro.
Ora, secondo Martin Kleppmann, informatico dell’Università di Cambridge, l’AI sta per cambiare radicalmente questa economia. Se gli LLM possono generare script di dimostrazione — e le ricerche del 2025-2026 mostrano che possono — il costo della verifica formale crolla. Il bello, come osserva Kleppmann, è che se l’AI produce una dimostrazione sbagliata, il proof checker la rifiuta automaticamente. Il verificatore umano deve solo controllare che la specifica sia corretta, non che la dimostrazione sia valida: un compito enormemente più semplice.
Il costo epistemico dell’efficienza
Questi due sviluppi — scoperta automatica e verifica automatica — pongono la matematica di fronte a un bivio culturale profondo. Il paradosso è che la macchina può produrre un risultato verificato come corretto senza che nessuno sappia spiegare perché funziona. Il matematico Akshay Venkatesh, medaglia Fields, ha espresso il timore che questa dinamica possa cancellare la comprensione intuitiva dalla pratica matematica: «Ci sono cose preziose nella nostra cultura che dovremmo cercare di preservare», ha detto.
Terence Tao è più possibilista ma non nega il problema. «Con questi strumenti si possono risolvere migliaia di problemi alla volta e iniziare a fare studi statistici», ha osservato. Il modo in cui la matematica viene fatta sta cambiando, ma cosa si perde e cosa si guadagna in questo passaggio è ancora da capire.
Comprensione e verificabilità: due processi separabili?
La storia della matematica è piena di risultati accettati prima di essere compresi. Nel XVII secolo, Leibniz e Newton usavano il calcolo infinitesimale senza disporre di una fondazione rigorosa; ci vollquero duecento anni perché Weierstrass mettesse ordine. Eppure la matematica funzionava. Il fisico Richard Feynman diceva di non capire l’elettrodinamica quantistica — nel senso che non aveva un’intuizione fisica chiara — eppure i suoi calcoli erano corretti.
Se l’AI può produrre dimostrazioni verificabili, forse la comprensione e la verificabilità possono essere processi separati. Non è necessariamente un dramma: la matematica è, in fondo, un sistema di relazioni formali. Ma c’è un rischio sottile. Se accettiamo risultati AI senza sviluppare l’intuizione di cosa significhino, costruiamo su fondamenta che non possiamo vedere. E quando qualcosa andrà storto — un risultato apparentemente corretto ma mal applicato — non avremo le antenne per accorgercene.
Verso una matematica a doppio binario
La direzione che si profila non è una matematica senza umani, né una matematica che ignora l’AI. È qualcosa di più simile a una collaborazione strutturata, dove il contributo umano si sposta progressivamente verso la formulazione delle domande giuste, la definizione delle specifiche, il controllo di coerenza filosofica. L’intelligenza artificiale genera, l’essere umano orienta e verifica — nel senso più profondo della parola.
La rivoluzione c’è stata. Non ha sostituito nessuno. Ma ha iniziato a cambiare il significato stesso di “fare matematica”, e nessuno ha ancora scritto il manuale per il mondo che viene dopo.
Fonti
- Quanta Magazine, “The AI Revolution in Math Has Arrived”, aprile 2025 — https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/
- Daniel Litt, analisi First Proof, febbraio 2026 — https://www.daniellitt.com/blog/2026/2/20/mathematics-in-the-library-of-babel
- Tao, Gómez-Serrano et al., “Mathematical Exploration and Discovery at Scale”, arXiv:2511.02864, novembre 2025
- Martin Kleppmann, “AI will make formal verification go mainstream”, dicembre 2025 — https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html
- Frontiers in AI, “Formal methods for safety-critical machine learning: a systematic literature review”, gennaio 2026 — https://www.frontiersin.org/journals/artificial-intelligence/articles/10.3389/frai.2026.1749956/full
- DARPA, “Math + AI = Tomorrow’s breakthroughs”, 2025 — https://www.darpa.mil/news/2025/math-ai-tomorrows-breakthroughs
Share this content:
