L’intelligenza artificiale (IA) è un modo semplificato di indicare un insieme di strumenti computazionali costruiti per svolgere compiti complessi in campo cognitivo. Qual è il ruolo di questi strumenti nella matematica attuale e futura? Cambierà il nostro modo di fare matematica e di immaginare nuovi filoni di ricerca? Giovanni Naldi riflette con un articolo in due puntate su alcuni aspetti legati all’uso dei computer e dell’IA in matematica. 

Fino a poco tempo fa si parlava di “pappagalli stocastici” per descrivere l’IA, ma oggi a che punto siamo? Gli annunci di nuovi traguardi raggiunti dall’intelligenza artificiale nel campo della matematica sono ormai all’ordine del giorno. La matematica, del resto, rappresenta un laboratorio ideale per questa sperimentazione, che mira (quasi sempre) a creare strumenti per generare, correggere o migliorare i software che usiamo ogni giorno o che controllano molti aspetti importanti di ciò che ci circonda.

Certo, un’allucinazione in un teorema matematico potrebbe preoccupare pochi eletti, ma un errore in un programma che controlla una diga, un sistema di sicurezza o una transazione bancaria preoccuperebbe chiunque. In questo scenario, sorgono spontanee diverse domande sul futuro del “mestiere” del matematico, con risposte spesso più urlate che ragionate. Avremo in futuro un compagno di studi artificiale? Già oggi deleghiamo volentieri molti compiti alle macchine, ma fin dove ci spingeremo? La disputa è aperta e per niente scontata.

In questo percorso diviso in due parti, proveremo a orientarci in un mondo dove le novità corrono più veloci della nostra capacità di analizzarle. Iniziamo ripercorrendo alcuni episodi chiave della storia dei programmi per la verifica e l’ausilio alla dimostrazione: un viaggio verso la formalizzazione della matematica, un desiderio molto più antico di quanto si possa immaginare.

Ufficio verifica dimostrazioni: siamo aperti

Possiamo immaginare la sorpresa degli affezionati lettori del blog di Kevin Buzzard (Xena Project, https://xenaproject.wordpress.com/) quando, nel dicembre 2020, si imbatterono in un post che non conteneva le consuete novità, bensì una sfida aperta lanciata da Peter Scholze (Medaglia Fields 2018). Fu l’inizio del Liquid Tensor Experiment.

La comunità raccolta attorno a quel blog si occupava, e si occupa tuttora, di formalizzazione matematica e sistemi di assistenza alle dimostrazioni. Scholze chiedeva la formalizzazione e la conseguente verifica formale di un teorema sviluppato con Dustin Clausen, apparso in alcune note non pubblicate sulla geometria analitica (titolo che non deve ingannare: sin dalle prime pagine ci si imbatte in un linguaggio estremamente astratto fatto di categorie e funtori, leggi qui per saperne di più).

Questo teorema rappresentava un tassello essenziale per la “matematica condensata”, una teoria in cui gli insiemi condensati prendono il posto dei classici spazi topologici. Uno degli scopi principali del progetto era riconciliare algebra e topologia. Informalmente, invece di definire uno spazio come un insieme di punti con una certa “forma”, lo si definisce considerando come una specifica classe di insiemi (gli insiemi profiniti) “vede” quello spazio.

Scholze sottolineava l’importanza cruciale del risultato: se il teorema avesse retto, avrebbe fornito un quadro rivoluzionario per l’analisi funzionale reale, trasformandola in una teoria essenzialmente algebrica. Il matematico confessava di aver trascorso gran parte del 2019 ossessionato dalla dimostrazione, arrivando a fissare un argomento su carta, ma con un’ombra di inquietudine: “Penso che nessun altro abbia osato guardare i dettagli e quindi ho ancora qualche piccolo, persistente dubbio”.

A rendere più urgente la richiesta era il ricordo di alcuni suoi errori passati, argomenti a prima vista persuasivi che si erano poi rivelati errati. Ritenendo questo teorema il suo risultato più importante, Scholze voleva la certezza assoluta della correttezza. Rivolgendosi alla comunità, dichiarò che la formalizzazione del teorema sarebbe stata un segnale inequivocabile: la verifica al computer della ricerca matematica più astratta era finalmente diventata possibile.

La sfida lanciata da Scholze non è rimasta inascoltata. A raccoglierla è stato un gruppo internazionale di matematici e informatici guidato da Johan Commelin. Il gruppo ha scelto di utilizzare Lean, un linguaggio di programmazione funzionale e assistente alla dimostrazione che stava rapidamente diventando lo standard per la formalizzazione della matematica avanzata. Il risultato è stato un successo: la comunità ha annunciato che il “cuore” della dimostrazione era stato completamente verificato. Il computer aveva analizzato ogni singolo passaggio logico, confermando che il dubbio di Scholze era infondato: il teorema era corretto.

Per Scholze, questo ha rappresentato la conferma che la parte centrale della sua teoria della “matematica condensata” poggiava su fondamenta solide. Il costo dell’impresa? Circa 40.000 righe di codice Lean e 18 mesi di lavoro intenso da parte di decine di collaboratori volontari da tutto il mondo. E’ stato anche un bel esperimento di matematica di gruppo, cosa molto strana per una attività di ricerca in matematica, anche grazie all’uso di “tactic” una funzionalità che permette di suddividere la dimostrazioni in risultati parziali e di operare su ciascuno di questi anche parallelamente. Le varie persone si sono interessate di qualche singolo risultato che ha contribuito al risultato finale.

Questo successo è stato salutato come un grande passo avanti nell’applicazione dell’intelligenza artificiale (IA) alla matematica. Tuttavia, occorre qui considerare l’apporto dell’IA in termini più ampi rispetto a quelli a cui siamo abituati (o “bombardati”) quotidianamente. Seguendo la proposta di Terence Tao e Tanya Klowden ( in questo nuovo e interessante articolo), con il termine IA ci si riferisce a un ampio spettro di strumenti informatici capaci di svolgere compiti cognitivi complessi. Questi includono sia le moderne tecnologie di apprendimento automatico, come i modelli linguistici e i modelli di diffusione per le immagini, sia forme di IA considerate più “tradizionali”, come i motori per il gioco degli scacchi o i dimostratori automatici di teoremi.

Riavvolgiamo il nastro, l’uso di strumenti computazionali in matematica ha seguito percorsi diversi nel tempo. Per esempio, le notti che Bryan John Birch e Peter Swinnerton‑Dyer passarono a Cambridge usando il computer EDSAC (impiegato di giorno per calcoli oceanografici) per esplorare il numero di soluzioni modulo p delle equazioni ellittiche \(y^2 = x^3 + ax + b\), con \(a, b\) razionali e condizione di non singolarità, ispirarono la celebre congettura che porta i loro nomi.

In un ambito diverso, all’inizio degli anni ’60 il meteorologo del MIT Edward N. Lorenz stava tentando di capire, attraverso modelli semplificati dell’atmosfera, perché le previsioni meteorologiche diventassero rapidamente inaffidabili. Quasi tutti i suoi colleghi ritenevano che il metodo statistico era sicuramente migliore dei metodi analitico-numerici. Dopo diverso tempo di studio, analisi e conti vari Lorenz ridusse il problema a tre equazioni differenziali che descrivevano la variazione del tempo di alcune variabili principali legate al fenomeno. In cerca di qualche test cruciale decise di avviare alcune simulazioni numeriche modificando i dati iniziali. Lorenz stesso racconta di aver avviato i test e di essersi assentato per circa un’ora a bersi un caffè. Al suo ritorno la sua sorpresa fu grande: i risultati mostravano che un modesto cambiamento dei dati iniziali, la cancellazione di poche cifre decimali, aveva prodotto un cambiamento molto significativo dei risultati. Ovviamente di fronte all’imprevisto scatta la domanda: perché? Un sistema fisico descritto da leggi deterministiche mostrava un comportamento casuale ed imprevedibile. La scoperta di Lorenz ha contribuito in modo decisivo a quella che oggi chiamiamo teoria del caos.

Molti ricercatori hanno usato esperimenti numerici e soluzioni particolari per guidare l’intuizione, cosa non sorprendente. Tuttavia, l’intervento dei computer nelle dimostrazioni di risultati importanti, prima ancora della formalizzazione completa, è spesso consistito nella generazione e nel controllo di un enorme numero di casi particolari, tipico di problemi con struttura discreta e aspetti combinatori. Due esempi classici sono il teorema dei quattro colori e la congettura di Keplero.

Nel primo caso, la dimostrazione pubblicata nel 1976 da Kenneth Appel e Wolfgang Haken confermò l’intuizione di Francis Guthrie: quattro colori bastano per colorare una mappa in modo che regioni adiacenti non abbiano lo stesso colore (Guthrie lo intuì colorando mappe di contee inglesi). La strategia della dimostrazione consisteva nel tradurre il problema in termini di grafi, mostrare che ci si poteva ricondurre ad un insieme finito di configurazioni “inevitabili”, verificare che ciascuna di queste ultime fosse riducibile a un caso noto o colorabile. La prova suscitò subito un acceso dibattito perché la parte sostanziale della verifica dei casi era affidata al calcolatore, rendendo la verifica manuale estremamente difficile. Non si trattava solo della grande quantità di configurazioni (la seconda parte, pubblicata nell’Illinois Journal of Mathematics, includeva 1476 casi distribuiti in più di 60 figure, non esattamente la situazione più coinvolgente di questo mondo), ma anche della preoccupazione che il programma usato potesse contenere errori. Spinti dalle critiche, Appel e Haken raffinarono e corressero dettagli, migliorarono algoritmi e verifiche. Successivamente, nel 1996, Robertson, Sanders, Seymour e Thomas fornirono una versione più snella della prova, con un insieme ridotto e meglio spiegato di configurazioni inevitabili e algoritmi più semplici e trasparenti. Infine, nel 2004, Georges Gonthier e collaboratori completarono la formalizzazione della dimostrazione in Coq (un altro sistema di assistenza automatica per le dimostrazioni), rendendola completamente verificabile meccanicamente: la prova computer‑assistita fu così tradotta in una prova formalmente controllabile.

La congettura di Keplero è un altro caso emblematico. L’idea nasce nel 1611, quando Johannes Keplero ipotizzò che l’impaccamento più denso di sfere (come le palle di cannone o le arance al mercato) fosse quello della struttura cubico‑facciale (la classica piramide a base quadrata). Dimostrare che non esistesse alcun metodo “più denso” richiese secoli. Nel 1998 Thomas Hales annunciò una soluzione: ridusse l’infinità delle possibili disposizioni a circa 5000 configurazioni specifiche e usò programmi per testare ciascuna configurazione mediante metodi basati sulla programmazione lineare. La dimostrazione comprendeva circa 250 pagine di testo più 3 gigabyte di dati e codice.

Hales inviò il lavoro agli Annals of Mathematics, il comitato di revisione lavorò per quattro anni senza poter verificare ogni singolo calcolo eseguito dal computer. La loro conclusione fu che erano “al 99% sicuri” della correttezza, ma non potevano garantirla totalmente perché era impossibile per un essere umano controllare tutti i calcoli. Questo generò uno stallo epistemologico: una dimostrazione può essere ritenuta tale se nessun essere umano è in grado di controllarla integralmente? Per risolvere la questione, Hales lanciò il progetto Flyspeck (Formal Proof of Kepler), con l’obiettivo di formalizzare l’intera dimostrazione in linguaggi comprensibili ai sistemi di verifica logica. Dopo oltre un decennio di lavoro, nel 2014 il gruppo di persone coinvolte nel progetto completò la verifica (qui l’articolo prodotto), usando HOL Light e Isabelle (altri due sistemi di verifica formale), solo allora la comunità matematica considerò la congettura definitivamente chiusa.

Cosa è cambiato, in sostanza? Prima (1998) il computer appariva come un servitore utile ma piuttosto limitato che produceva risultati di cui bisognava fidarsi, spesso con scetticismo; dopo (2014 e oltre), attraverso la formalizzazione, il computer può svolgere il ruolo di “notaio logico”, fornendo una prova che ogni passaggio del ragionamento è formalmente corretto. Il passaggio dalla semplice computazione (effettuare calcoli pesanti) alla formalizzazione (verificare automaticamente la correttezza logica) è al cuore della trasformazione che stiamo descrivendo.

Formalizzare la matematica significa tradurre definizioni, enunciati e dimostrazioni dal linguaggio naturale in un linguaggio formale preciso che un sistema computazionale può leggere e verificare senza ambiguità. Gli ingredienti principali sono: un linguaggio formale che esprime oggetti matematici (numeri, insiemi, funzioni, spazi ecc.) ed enunciati (teoremi, lemmi); un sistema di regole e assiomi su cui si costruiscono le prove; la rappresentazione della dimostrazione come oggetto formale; e un “kernel”, componente minimale e fidato, che controlla che ogni passo derivi correttamente dalle regole. I vantaggi sono l’eliminazione di ambiguità e lacune e la possibilità di verificare automaticamente anche calcoli numerici lunghi, ovviamente fidandosi del kernel.

Un problema pratico emerso in molte formalizzazioni recenti, come nel celebre Liquid Tensor Experiment, è la necessità di colmare le lacune logiche che, negli scritti originali, venivano liquidate con espressioni come «è ovvio che» o «si verifica facilmente». Per un computer, però, nulla è ovvio. Formalizzare non significa scansionare un libro, ma definire ogni concetto intermedio senza dare nulla per scontato. In questo senso, la formalizzazione rende «visibile» la matematica che spesso rimane implicita ed “invisibile”, come nota con efficacia la matematica Emily Riehl: è un processo che estrae la struttura profonda dal linguaggio naturale.

Questo enorme sforzo di digitalizzazione ha un valore aggiunto fondamentale: la riutilizzabilità. Una volta formalizzati, risultati e costruzioni diventano “mattoni” pronti per essere impiegati in altri sistemi o dimostrazioni future. Non è un caso se un progetto guidato da Kevin Buzzard (Imperial College London) miri oggi a formalizzare l’Ultimo Teorema di Fermat utilizzando Lean. La monumentale dimostrazione di Andrew Wiles e Richard Taylor coinvolge ambiti vastissimi: dalla teoria dei numeri alla geometria algebrica, fino all’analisi armonica.

Lo scopo del progetto non è tanto verificare la correttezza di Wiles (ritenuta ormai solida), quanto produrre una libreria digitale di oggetti matematici moderni. Attraverso il software blueprint sviluppato da Patrick Massot, il progetto genera una mappa concettuale strutturata, un grafo delle dipendenze, che permette di visualizzare lo stato di avanzamento. Questo approccio modulare è rivoluzionario: consente ai matematici di collaborare alla formalizzazione senza dover padroneggiare l’intera, complessa dimostrazione.

I sostenitori di questo approccio sottolineano come un archivio formalizzato offra un riferimento privo di errori per studenti e ricercatori. In futuro, questi strumenti aiuteranno gli autori a evitare affermazioni false e le case editrici a validare teoremi estremamente complessi. Tuttavia, la strada verso l’efficienza è ancora in salita. Formalizzare un teorema rilevante richiede mesi o anni. La frontiera attuale è l’auto-formalizzazione, ovvero l’uso di IA per tradurre automaticamente il linguaggio matematico (codificato con sistemi molto diffusi come LaTeX) in codice formale.

Molti settori non hanno ancora librerie complete; spesso i ricercatori devono “ricostruire da zero” concetti banali. Ovviamente ci si deve poi fidare del kernel (il cuore del software che controlla la logica). Per questo si preferiscono kernel piccoli e verifiche incrociate tra sistemi diversi. In ogni caso l’integrazione nei flussi editoriali è lontana: mancano protocolli per sottomettere dimostrazioni formalizzate e restano aperte questioni legali sulla proprietà dei dati e dei risultati.

L’idea di ridurre il ragionamento a procedure meccaniche ha radici profonde. Già nel XVII secolo, Leibniz immaginava il calculus ratiocinator, un linguaggio simbolico per risolvere ogni disputa al grido di: «Calculemus!» (calcoliamo). Secoli dopo, stiamo saltando molti fatti e persone, David Hilbert propose un programma per dare alla matematica una certezza assoluta contro paradossi e antinomie. I moderni sistemi di formalizzazione sono, di fatto, la realizzazione del sogno di Hilbert.

Ma perché tanto interesse per la matematica pura da parte del mondo tecnologico? La risposta risiede nell’informatica critica. Un programma può essere trattato come un teorema: dimostrare che un software non fallirà mai è la stessa cosa di dimostrare un enunciato logico. Questo legame è noto come Isomorfismo di Curry-Howard: scrivere una dimostrazione corretta e scrivere un programma privo di bug sono, in un certo senso, la stessa operazione.

All’orizzonte si prospettano problemi diversi e altre possibilità, come afferma Terence Tao: “Ho l’impressione che l’IA non sia semplicemente un’altra tecnologia come il word processor o il browser web. Sta davvero costringendoci a ripensare questioni fondamentali, che cos’è una dimostrazione matematica? Che cos’è un articolo scientifico? Qual è lo scopo della nostra professione? Se non ci poniamo noi stessi queste domande, allora verranno risolte al posto nostro da un’azienda tecnologica o determinate da incentivi finanziari. Dobbiamo muoverci in anticipo.” (in questo articolo).

Il discorso va approfondito.

1-continua

Giovanni Naldi

Immagine di copertina: Photo by Jayson Hinrichsen on Unsplash