Nei primi giorni di settembre 2026, due annunci hanno dato l’impressione che il futuro della matematica fosse arrivato tutto d’un colpo^[1].

Anthropic ha comunicato che un insieme di agenti Claude ha prodotto la prima dimostrazione completa dell’“ultimo teorema di Fermat” verificata da un computer. Andrew Wiles (con il successivo contributo di Richard Taylor) aveva già risolto il problema negli anni Novanta. Il teorema in questione afferma che non esistono numeri interi positivi che soddisfano l’equazione aⁿ+bⁿ=cⁿ (mentre per n=1 e n=2 tail soluzioni esistono). Il risultato reclamato da Anthropic consiste nel ricostruirlo in modo puramente formale in Lean, uno dei più noti sistemi di dimostrazione interattiva (interactive theorem provers). Per arrivarci, gli agenti di Claude ci hanno messo 11 giorni, generando circa 13 milioni di righe di codice.

Quattro giorni dopo, OpenAI ha annunciato che un sistema costituito da migliaia di agenti ha trovato una costruzione che, secondo OpenAI, trova una risposta a uno dei problemi del millennio formulato dal Clay Mathematics Institute, quello relativo all’esistenza e regolarità delle equazioni di Navier-Stokes. Queste equazioni descrivono il moto di un fluido approssimandolo con un mezzo continuo, piuttosto che ricostruirlo dal movimento delle singole molecole che lo compongono. Questa approssimazione si è rilevata molto robusta e le equazioni vengono usate per progettare aerei, formulare previsioni meteorologiche o studiare il moto di fiumi o del flusso sanguigno. Tuttavia, non è mai stato dimostrato che esistano soluzioni “regolari” per qualsiasi valore della velocità iniziale del fluido e della forza a cui esso è sottoposto – due delle componenti che definiscono le equazioni. Per regolari, si intendono soluzioni in cui la velocità non tende all’infinito in un tempo finito. Visto che questo fenomeno non è mai stato osservato in nessun fluido, se questo accadesse segnalerebbe che l’approssimazione al continuo non è sempre valida. OpenAI ha pubblicato un articolo di 166 pagine e una formalizzazione in Lean, ma le verifiche indipendenti sono ancora in corso.

Pur facendo entrambi un uso centrale di Lean, i risultati presentano una differenza importante. Nel caso di Fermat, il problema era chiuso da tre decenni e la macchina si è limitata, per così dire, a svolgere un’enorme opera di ricostruzione formale. Nel caso di Navier–Stokes, invece, si potrebbe sostenere che la macchina abbia concorso alla scoperta della risposta al problema, oltre a contribuire alla sua certificazione. Tuttavia, in entrambi i casi si trova una dimostrazione formale elaborata e verificata meccanicamente.

Una delle ragioni per cui le notizie sono state accompagnate da un profluvio di reazioni è certamente il posto che la matematica occupa nell’immaginario comune. Una macchina che classifica immagini può essere utile, e una che produce musica gradevole può risultare inquietante. Ma una macchina che dimostra problemi aperti in matematica entra di prepotenza nel territorio marcato da un tipo di intelligenza che è distribuita con parsimonia tra gli umani.^[2]

Eppure, dimostrazioni generate, assistite o controllate da macchine non sono certo appannaggio degli ultimi, costosissimi, modelli di OpenAI o Anthropic. Sono l’esito, per certi aspetti tardivo, di un progetto iniziato prima che esistessero i calcolatori elettronici. Buona parte della logica matematica contemporanea è nata esattamente per trasformare dimostrazioni matematiche guidate dall’intuizione umana, in oggetti formali in cui l’intuizione non aveva più alcun ruolo, e quindi suscettibili di controllo meccanico. Vista in questa prospettiva più lunga, la notizia assume un tono diverso: entro i limiti assoluti stabiliti negli anni 30 del Novecento da Kurt Gödel e Alan Turing, una parte di un programma di ricerca lungo un secolo sembra finalmente avviarsi verso il raggiungimento di risultati concreti. La questione interessante è capire quale parte.

Il sogno di un motore per le dimostrazioni

Per gran parte della storia della matematica, la dimostrazione aveva lo scopo di convincere (sé stessi, e poi gli altri) della correttezza della propria argomentazione, e in particolare della sua conclusione – ciò che comunemente chiamiamo teorema. Si trattava tuttavia di un argomento elaborato per la fruizione dei pari. Euclide, tra i primi a prendere le dimostrazioni sul serio, non registrava tutti i singoli passaggi della propria argomentazione, ma si fermava lì dove riteneva il livello di dettaglio sufficiente affinché i suoi lettori potessero capire perché l’argomento funzionasse. La quasi totalità delle dimostrazioni matematiche ha ancora questo stile.

Fanno eccezione le dimostrazioni formali, elaborate all’interno di quell’area particolare della matematica che studia, ehm, le dimostrazioni matematiche. Si tratta dell’area della logica oggi nota come teoria della dimostrazione, le cui premesse si svilupparono tra la fine dell’Ottocento e i primi decenni del Novecento, con l’obiettivo di purgare l’argomentazione matematica dalla sua dipendenza dall’intuizione di chi la legge. Gottlob Frege ideò un linguaggio formale nel quale la struttura logica di un’inferenza potesse essere scritta esplicitamente. Bertrand Russell e Alfred North Whitehead, sviluppando idee molto feconde di Giuseppe Peano, concretizzarono l’ambizione nei tre monumentali volumi dei Principia Mathematica (1910–1913). La scommessa era che la matematica (cosiddetta pura) potesse essere definita mediante un numero molto ridotto di concetti logici e derivata da un insieme altrettanto ristretto di principi logici.^[3]

Lo scopo, che ai più sembrava bizzarro, fu ampiamente frainteso. Notevole il disprezzo per la “logistique” espresso da Poincaré, che retoricamente si chiedeva quante equazioni sarebbero servite a Russell e Whitehead per dimostrare un “vero teorema” visto che gliene servivano 27 per asserire che 1 è un numero. Anche i giganti prendono cantonate. Il punto non era dimostrare “meglio” i teoremi, ma renderne completamente esplicito ogni passaggio. In una dimostrazione informale — quelle che si trovano nei libri di testo dalle superiori in su — contenuto matematico e inferenza logica si presentano intrecciati. Chi legge forma un’intuizione su cerchi, numeri primi o funzioni mentre completa implicitamente i passaggi mancanti. (Si tratta questa di una fonte inesauribile di frustrazione per chi studia su libri che non dedicano abbastanza spazio all’idea della dimostrazione.) Una dimostrazione formale invece separa le mosse inferenziali consentite dalla logica, dal contenuto matematico a cui vengono applicate. Questa separazione richiede la definizione rigorosa di una sintassi in cui sono costruiti gli assiomi e le regole di inferenza. I primi forniscono i punti di partenza, mentre le seconde specificano esattamente i passi inferenziali ammissibili, e cioè quali espressioni formali seguono da quali altre. Così formulata, una dimostrazione è una sequenza finita di passi, ognuno dei quali è univocamente giustificato dalle regole del sistema. Russell e Whitehead ragionavano così mezzo secolo prima che venisse costruito un computer, e senza saperlo contribuivano a precisare ciò di cui un verificatore automatico di dimostrazioni avrebbe avuto bisogno.

David Hilbert dette al progetto un impulso decisivo, in parte dovuto anche alla sua statura matematica, suggerendo che gli stessi sistemi formali dovessero essere trattati come oggetti matematici. La retorica di Hilbert non nascondeva la grandiosità del progetto. Nel suo Pensiero assiomatico del 1918 scriveva che “tutto ciò che può essere oggetto del pensiero scientifico […] approda al metodo assiomatico”. Suggeriva che lo stesso concetto di dimostrazione matematica diventasse oggetto d’indagine, così come in fisica si studiano gli strumenti e non ci si limita a usarli. Fece una lista di domande che si sono rivelate centrali allo sviluppo della matematica computazionale, tra cui: Il risultato di una dimostrazione può essere verificato? Esiste un criterio per la semplicità di una dimostrazione? Un problema matematico può essere deciso mediante un numero finito di operazioni?^[4]

Per cogliere la rilevanza di queste idee per la dimostrazione automatica è utile pensare ad assiomatizzazione, formalizzazione e automazione come distinte ma collegate in questo modo. L’assiomatizzazione individua le assunzioni matematicamente interessanti e licenzia le loro conseguenze puramente logiche. La formalizzazione codifica linguaggio e inferenze con precisione sufficiente a rendere superflua qualsiasi forma di comprensione o intuizione da parte di chi verifica la dimostrazione. L’automazione affida a una macchina il (o una parte del) lavoro che ne deriva. L’assiomatizzazione è necessaria alla formalizzazione che a sua volta rende possibile l’automazione.

Il contributo di Turing

Prima di Alan Turing, gli algoritmi si presentavano in forma concreta, per risolvere cioè problemi specifici come, per esempio, il calcolo del minimo comune multiplo tra due numeri. Ciò che accomunava i diversi algoritmi sembrava intuitivamente chiaro: procedono per passi discreti; ogni passo determina univocamente il successivo; una volta avviata la procedura, non occorre più alcuna comprensione di quello che si sta facendo.

Nel 1936, Alan Turing aveva però bisogno di una definizione rigorosa, perché si era chiesto se esistessero problemi non risolvibili algoritmicamente. Per formulare il problema propose di identificare una qualsiasi “procedura meccanica” con un dispositivo immaginario dotato di un nastro suddiviso in celle, una testina capace di leggere o scrivere un simbolo, un elenco finito di stati interni e regole che indicavano quale operazione eseguire. Oggi la chiamiamo Macchina di Turing. La sua forza è per così dire nella sua l’austerità, ottenuta riducendo all’ essenziale ogni singola azione che secondo Turing caratterizzava l’attività umana del computare. Congetturò che mettendo insieme una serie arbitrariamente lunga di queste operazioni elementari si poteva realizzare qualsiasi procedura meccanica.

Turing rese universale l’idea concreta di algoritmo. Invece di costruire un dispositivo per l’addizione, un altro per l’algebra e un altro ancora per la logica, pensò che si potesse collocare sul nastro della macchina universale la descrizione di una macchina specializzata. Le istruzioni diventavano dunque dati. Poiché una dimostrazione formale è una sequenza di passi governati da regole e la macchina di Turing catturava il significato di un processo formale governato da regole, in linea di principio, una macchina di Turing poteva enumerare le dimostrazioni, cercare fra esse e controllarne una proposta.

I primi risultati

A metà degli anni Cinquanta, Allen Newell, Herbert Simon e Cliff Shaw costruirono il Logic Theorist, un programma che cercava dimostrazioni di proposizioni tratte dai Principia Mathematica, trasformando strutture simboliche secondo regole logiche. In ogni momento erano disponibili molte mosse lecite, ma pochissime conducevano in modo relativamente diretto al teorema. Il programma impiegava quindi euristiche per scegliere i percorsi promettenti.^[5] Poco dopo, ma con un approccio molto diverso, Hao Wang ottenne un risultato sbalorditivo per i tempi. I suoi programmi furono infatti capaci di dimostrare quasi quattrocento teoremi logici dei Principia, con tempi dell’ordine di pochi minuti. Era il 1956.

È interessante notare come Logic Theorist contenesse già l’architettura di base degli odierni sistemi di dimostrazione automatica, tra cui un generatore che propone la mossa successiva e un sistema formale che rifiuta le mosse illegali. I progressi tecnologici dell’ultimo decennio hanno migliorato incredibilmente l’efficacia di queste componenti, ma queste sono presenti da almeno settant’anni.

La nicchia in cui è nato Lean

Logic Theorist rappresentava uno dei due filoni in cui l’idea di meccanizzare le dimostrazioni si sarebbe successivamente sviluppata. Nella dimostrazione automatica si chiede al software di trovare una dimostrazione per un’asserzione data. Nella dimostrazione interattiva si pone invece l’accento sulla costruzione guidata e sulla verifica del risultato. Qui il software “chiede” che ogni affermazione sia sostenuta da definizioni, teoremi precedenti e assiomi. Tuttavia, la distinzione tra dimostratori automatici e interattivi è diventata col tempo molto sfumata. Dall’Automath di Nicolaas de Bruijn negli anni Sessanta a sistemi come LCF, Coq, HOL e Isabelle, i progettisti hanno sperimentato combinazioni diverse di linguaggi formali espressivi, guida umana, ricerca automatica e grandi librerie di teoremi. Lean si sviluppa in questo ambiente. In una descrizione del sistema pubblicata nel 2015, Leonardo de Moura e i suoi collaboratori lo presentarono come un “dimostratore di teoremi open source progettato esplicitamente per colmare la distanza fra dimostrazione automatica e interattiva”.^[6]

Nella notizia relativa al teorema di Fermat, Lean è stato il linguaggio in cui è stata formalizzata la dimostrazione del teorema, l’ambiente di lavoro in cui è stata riprodotta e il verificatore finale che ne ha certificato la correttezza. Nel problema del millennio su Navier–Stokes, OpenAI riferisce che i suoi agenti sono arrivati prima alla costruzione analitica del risultato, la cui formalizzazione e verifica in Lean hanno richiesto 17 ore. Lean non viene dunque indicato come l’origine della costruzione, ma ha fornito una seconda rappresentazione esplicita dell’argomento e prodotto un certificato di validità che altri possono replicare in modo indipendente.

E il teorema di Gödel?

Se pensiamo a questi successi dei sistemi di IA come alla realizzazione delle ambizioni di Hilbert, non possiamo non chiederci quale significato da’ questo nuovo contesto ai celebri teoremi di Gödel.

Rispondendo direttamente a un problema sollevato da Hilbert, nel 1931 Kurt Gödel mostrò che i sistemi formali abbastanza ricchi per esprimere l’aritmetica elementare non possono essere al tempo stesso coerenti (cioè incapaci di dimostrare contraddizioni) e completi (cioè capaci di dimostrare tutte le cose vere). In un sistema coerente di questo tipo esistono quindi enunciati aritmetici veri che non possono essere dimostrati con i mezzi del sistema. Colpendo ciò che più stava a cuore a Hilbert, Gödel dimostrò inoltre che un sistema del genere, se coerente, non può dimostrare la propria coerenza.^[7]

Si tratta di un limite invalicabile per ogni sistema formale per la matematica, ma non di un divieto di costruire verificatori e dimostratori utili. Al contrario, le notizie di questo settembre ci dicono non soltanto che le macchine possono verificare teoremi “difficili” (cosa che non è impedita dai teoremi di Gödel) ma che le macchine possono anche (contribuire a) dimostrarli. Mentre i teoremi di Gödel asseriscono qualcosa di universale, gli assistenti alla dimostrazione lavorano in uno spazio delimitato. Questo può richiedere un numero esorbitante di passi inferenziali, ed è qui che i progressi tecnologici dell’ultimo decennio fanno la differenza. Gödel, dunque, non ha reso impossibile l’arrivo dei matematici artificiali. I suoi risultati hanno stabilito che nessun dimostratore fissato una volta per tutte coincide con la matematica stessa, ma localmente, dentro i sistemi formali, e “fra un sistema e l’altro”, rimane un territorio che è oggi sembra essere ampiamente alla portata delle macchine.

Cosa resta a chi fa ricerca matematica?

È ovviamente molto difficile capire l’impatto di questi (e presumibilmente i futuri) risultati nella pratica matematica di tutti i giorni. In modo preliminare è tuttavia utile distinguere due aspetti che tipicamente coesistono in una dimostrazione degna di nota.

Il primo ha a che fare con l’intuizione matematica. È questa che fa trovare una definizione feconda, riconoscere una regolarità, o capire che un problema o una tecnica possono essere trasferiti da un campo a un altro. L’intuizione fornisce l’idea attorno alla quale una dimostrazione può articolarsi. Il secondo ha a che fare con la competenza tecnica. Si tratta di ciò che permette di mettere quell’idea a frutto sviluppandone le conseguenze e colmando le lacune. La competenza tecnica trasforma un’intuizione promettente in una dimostrazione valida.

I due aspetti non sono in conflitto, tutt’altro. Le dimostrazioni sono tanto più apprezzate quanto sono capaci di spiegare l’idea, anziché seppellirla sotto una colata di formule. La distinzione chiarisce anche alcuni aspetti dei due annunci di settembre. A prima vista, la formalizzazione di Fermat è un trionfo della competenza tecnica. Gli agenti Claude non hanno sostituito le idee di Wiles, ma le hanno ricostruite con un dettaglio inimmaginabile per qualsiasi essere umano. Eppure, persino questo lavoro meccanico richiede di decidere come suddividere il problema, quali teoremi intermedi dimostrare e come esprimere la matematica consueta nelle librerie utilizzabili da Lean.

Il risultato su Navier–Stokes attraversa la linea che separa tecnica e intuizione nella direzione opposta. Secondo il resoconto di OpenAI, gruppi di agenti hanno esplorato approcci, scambiato risultati intermedi utili e infine elaborato una costruzione del controesempio cercato. Lean sembrerebbe invece aver svolto una funzione di auditing: non è stato, secondo il resoconto pubblicato, la fonte dell’idea, ma il linguaggio nel quale le sue conseguenze logiche sono state rese esplicite e controllate.

Il feedback fra generazione e verifica altera l’immagine secondo cui gli esseri umani producono idee matematiche che le macchine poi si limitano a controllare. Un sistema che genera dimostrazioni può usare un verificatore come una persona che fa matematica usa la lavagna. La verifica può così diventare parte dell’idea.

Da strumento a collega

Alan Turing anticipò questo argomento quando i calcolatori elettronici programmabili muovevano i primi, incerti passi. In una lezione del 1947 immagina le persone al lavoro con l’allora avveniristico Automatic Computing Engine nei ruoli di “padroni” e “servitori”. I padroni avrebbero ideato tavole di istruzioni sempre più profonde mentre i servitori avrebbero inserito le schede, riparato i guasti e fornito i dati. Turing intuì che il calcolatore avrebbe gradualmente assunto entrambi i ruoli, non appena le relative tecniche fossero diventate sufficientemente formalizzate e i problemi di memoria (storage) fossero stati risolti efficacemente.

Riguardo al rapporto tra persone e macchine impegnate nella risoluzione di un problema matematico, Turing osserva che l’intenzione originaria fosse “trattarli come schiavi”, assegnando ai calcolatori soltanto compiti il cui funzionamento l’essere umano di turno comprendeva completamente, ma trovava troppo noiosi e ripetitivi per meritare il suo lavoro. Ma Turing si chiede se le macchine dovessero essere impiegate sempre in quel modo. Chiede allora al suo pubblico di supporre che una macchina possa modificare le proprie istruzioni, migliorare con l’esperienza e compiere progressi che il progettista non aveva previsto. In quel caso, suggerisce Turing, il calcolatore assomiglierebbe a un allievo che ha imparato dal maestro, e che poi ha aggiunto qualcosa con il proprio lavoro. Turing continua chiedendo che alle macchine sia concesso un “fair play”: anche gli esseri umani commettono errori quando sperimentano tecniche nuove, e la fallibilità non dovrebbe quindi escludere una macchina dall’intelligenza.^[8]

Nel 2017, Sven Delarivière e Bart Van Kerkhove hanno dato un nome efficace a questa possibilità. Il loro “matematico artificiale” (artificial mathematician) non era semplicemente un software impiegato all’interno di una dimostrazione. Era un possibile partecipante alla pratica matematica: “non soltanto come metodo d’indagine, ma come collega d’indagine”.^[9] Sostenevano che l’obiezione centrale alla realizzazione dei matematici artificiali non consistesse nella fallibilità dei computer o nella lunghezza eccessiva delle loro dimostrazioni. Come notava Turing settant’anni prima, anche i matematici sbagliano, dipendono dalle affermazioni altrui e spesso dedicano anni a lavori che soltanto pochi specialisti sono in grado di capire e controllare. L’obiezione più profonda era che le macchine manipolassero simboli senza comprenderli. Delarivière e Van Kerkhove ipotizzavano che il progresso richiedesse sistemi distribuiti di agenti specializzati capaci di competere, cooperare, riconoscere schemi, rivedere tentativi parziali e imparare dall’esperienza. La somiglianza con gli agenti di Claude e OpenAI che hanno fatto notizia in questi giorni è evidente.

Spostare l’asticella sempre un po’ più in su

Dopo i successi degli anni Cinquanta, la domanda sull’esistenza dei matematici artificiali è stata formulata chiedendo se un computer potesse produrre dimostrazioni rilevanti per la ricerca e la pratica matematica che gli esseri umani non avessero già elaborato. Dopo l’esempio del teorema dei quattro colori dimostrato a metà degli anni settanta, le risposte non sembravano arrivare con la frequenza sperata. Oggi non è più così, o almeno esistono candidati molto seri.

È verosimile che sposteremo presto l’asticella ancora un po’ più in su, aspettandoci che le macchine sappiano aiutarci a (o sappiano autonomamente) individuare un problema interessante, o valutare la fecondità di una direzione di ricerca.

Inevitabilmente sono domande che intersecano il concetto di autorialità, che già emergono e causano molte reazioni sui due casi qui considerati. La formalizzazione di Fermat dipende non solo da secoli di teoria dei numeri difficilmente attribuibili, e dal lavoro originale di Wiles e Taylor, ma anche dalle esposizioni successive che ne sono state fatte negli ultimi tre decenni, da tutto il lavoro che ha portato a Lean, dal lavoro che ha portato a Mathlib, dalla piattaforma che ha coordinato gli agenti e da molti altri fattori. Stessa cosa per il problema su Navier–Stokes. Se verificato, a chi dovrebbe essere assegnato il milione di dollari messo in palio dal Clay Institute? Come anticipato da Turing, potrebbe non esistere affatto il punto in cui l’ingegno umano consegna il suo prodotto finito all’azione meccanica.

Hume vindicatus

I successi annunciati da Anthropic e OpenAI possono dunque essere letti in molti modi. Visti attraverso la lunga storia delle idee da cui si sono originati, è plausibile che il loro effetto sia quello di alzare di un bel po’ l’asticella. Se riusciamo a farci assistere efficacemente dai sistemi di intelligenza artificiale per formalizzare, stabilire e verificare risultati matematici “seri”, allora l’avanzamento della conoscenza matematica sarà sempre più legato alla scelta e alla formulazione dei problemi, cioè alla congettura e al ragionamento plausibile guidati dall’intuito matematico. Non a caso, si tratta di quella parte di attività matematica che la dimostrazione formale espunge programmaticamente dal suo orizzonte. Ma le osservazioni di Turing sul rapporto padrone-servitore ci mettono in guardia dal ritenere che si tratti di compiti perennemente inaccessibili alle macchine. In questo senso, i risultati di Anthropic e OpenAI mostrano che il confine tra idea e tecnica è già sufficientemente poroso da permettere alle macchine di attraversarlo in entrambe le direzioni.

Ora, se la macchina si affranca dal suo ruolo di servitrice tecnica per conquistare quello di padrona dell’idea matematica, si potrebbe concludere che di matematiche e matematici in carne e ossa ci sarà sempre meno bisogno. Può darsi. Tuttavia, trovo più interessante un’altra interpretazione dei fatti anticipata nel 2024 da Gabriele Lolli in La creatività in matematica. Ribaltando completamente il punto di vista, Lolli osservava che la collaborazione tra logica [e] probabilità […] che si materializza con la dimostrazione interattiva “introduce un elemento veramente nuovo nella matematica e più in generale nella concezione della razionalità. Il carattere essenzialmente probabilistico, ma altamente affidabile (quanto si vuole), delle prove prodotte dalle nuove tecniche manifesta in modo evidente la natura semplicemente non sovrumana della conoscenza matematica, come di ogni altra forma di conoscenza: Hume vindicatus.”

Suggerimenti bibliografici

• Kevin Hartnett, The Proof in the Code: How a Truth Machine Is Transforming Math and AI (Quanta Books, 2026). Ricostruzione molto dettagliata, a tratti avvincente, della storia di Lean e della comunità che ha portato la dimostrazione verificata da computer nel cuore della matematica contemporanea.
• Gabriele Lolli, Matematica in movimento. Come cambiano le dimostrazioni (Bollati Boringhieri, 2022). Una riflessione matematica, storica e filosofica sull’evoluzione delle forme della dimostrazione matematica.
• Gabriele Lolli, La creatività in matematica (Bollati Boringhieri, 2024). Una riflessione sulla scoperta, sull’invenzione e sulla creatività nella pratica matematica che abbraccia tanto il rapporto della matematica con la letteratura, quanto quello della matematica con le macchine.
• Giuseppe Primiero, On the Foundations of Computing (Oxford University Press, 2019). Presentazione accademica di taglio storico e concettuale della computazione come pratica matematica, ingegneristica e sperimentale.

Note

1. OpenAI, “On the Navier–Stokes Millennium Prize Problem”, 8 settembre 2026, e Finite Time Blowup for Navier–Stokes, 2026; Charles L. Fefferman, “Existence and Smoothness of the Navier–Stokes Equation”, formulazione ufficiale del Millennium Prize Problem; Anthropic, “Formalizing Fermat’s Last Theorem”, 4 settembre 2026. Si tratta di risultati appena annunciati. Il risultato di OpenAI riguarda esplicitamente le alternative (C) e (D) della formulazione ufficiale, cioè il caso con forzante esterna liscia. Al 12 settembre 2026, la pagina dedicata a Navier–Stokes del Clay Mathematics Institute continuava a classificare il problema fra quelli non risolti; la formulazione adottata nel testo distingue quindi la tesi proposta e la sua verifica formale dall’accettazione indipendente. ↩
2. Su questo punto un numero importante di medaglie Fields guidate da Terry Tao si è espressa in modo molto critico attraverso la dichiarazione “A Severe Misalignment of AI in Mathematics”. I firmatari sostengono che l’uso della soluzione di problemi matematici aperti come benchmark per i sistemi di IA (e per il loro marketing) è incompatibile con alcuni degli obiettivi fondamentali della comunità matematica: la comprensione concettuale, lo sviluppo e la trasmissione di nuovi metodi, la formazione e la corretta attribuzione del lavoro precedente. In particolare, richiama l’attenzione sul rischio che soluzioni prodotte e annunciate a grande velocità non lascino il tempo necessario per l’esposizione, la verifica, l’individuazione delle idee nuove e la loro integrazione nel sapere matematico condiviso. ↩
3. Bertrand Russell, “Mathematical Logic as Based on the Theory of Types” (1908), in Jean van Heijenoort, a cura di, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (Harvard University Press, 2002), pp. 152–182. ↩
4. David Hilbert, “Axiomatic Thinking” (1918), traduzione inglese in Philosophia Mathematica, s1-7, nn. 1–2 (1970), pp. 1–12. ↩
5. Allen Newell, J. C. Shaw e Herbert A. Simon, “Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics”, Proceedings of the Western Joint Computer Conference (1957), pp. 218–230; Hao Wang, “Toward Mechanical Mathematics”, IBM Journal of Research and Development 4, n. 1 (1960), pp. 2–22. ↩
6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn e Jakob von Raumer, “The Lean Theorem Prover (System Description)”, in Automated Deduction — CADE-25, Lecture Notes in Computer Science 9195 (Springer, 2015), pp. 378–388. ↩

7. Kurt Gödel, “On Formally Undecidable Propositions of Principia Mathematica and Related Systems I” (1931), in Jean van Heijenoort, a cura di, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (Harvard University Press, 2002), pp. 596–616. ↩

8. Alan M. Turing, “Lecture to the London Mathematical Society on 20 February 1947”, in The Collected Works of A. M. Turing: Mechanical Intelligence, a cura di D. C. Ince (North-Holland, 1992). ↩
9. Sven Delarivière e Bart Van Kerkhove, “The ‘Artificial Mathematician’ Objection: Exploring the (Im)possibility of Automating Mathematical Understanding”, in Bharath Sriraman, a cura di, Humanizing Mathematics and Its Philosophy (Birkhäuser/Springer, 2017), pp. 173–198. ↩