La matematica sta cambiando con l’intelligenza artificiale. È un caso l’ultimo teorema dimostrato con l’IA da Giorgio Parisi. In un recente articolo su Quanta si è parlato di questa nuova collaborazione, attraverso una figura che ne è ormai diventata l’emblema: Terence Tao. Di queste prospettive ce ne parla Marco Menale.

Giorgio Parisi ha usato l’intelligenza artificiale per dimostrare un teorema in un articolo, con Francesco Zamponi, apparso su arxiv il 2 giugno. Sì, parliamo proprio del fisico premio Nobel 2021. Per la precisione, hanno usato Sonnet 4.6 e Opus 4.7. La notizia è andato molto in giro e ha colpito parecchie persone, forse anche quelle più scettiche. E se n’è parlato al grande pubblico: sui giornali e non solo. Il podcast “Ci Vuole una Scienza” ci ha dedicato la puntata “Le AI stanno cambiando la matematica”. Quella che in Italia è suonata come una grossa novità in realtà va consolidandosi da anni con uno dei più grandi matematici del secolo: Terence Tao.

Medaglia Fields nel 2006, autore di tanti (e fidatevi che il corsivo non basta!) e d’impatto lavori scientifici, Terence Tao è noto non soltanto per i suoi risultati matematici, ma anche per un’altra caratteristica: la capacità di collaborare. Nel corso della sua carriera ha scritto articoli con oltre duecento coautori. Tra questi non c’è Paul Erdős, anche se c’è una foto che lo ritrae assieme a un Tao bambino. E questa foto ha un che di emblematico, poiché il matematico ungherese ha trasformato la collaborazione scientifica in una vera filosofia della ricerca. Inoltre, Tao è famoso per il suo blog pieno di tanta, profonda, matematica.

La matematica come impresa collettiva raggiunge una nuova dimensione nel 2009, quando Tao partecipa al progetto Polymath, progetto avviato dal matematico britannico Sir Timothy Gowers. L’obiettivo è tanto semplice quanto rivoluzionario: utilizzare la rete internet per permettere a decine di matematici di affrontare insieme problemi aperti. Invece di lavorare in isolamento, i partecipanti condividono pubblicamente intuizioni, osservazioni e risultati parziali. Una sorta di live-blog della ricerca. Un’idea può suggerirne un’altra, fino a costruire collettivamente una soluzione completa. Polymath dimostra che problemi matematici complessi possono essere scomposti in una moltitudine di problemi più piccoli, affrontabili da persone diverse.

Da internet si passa poi all’intelligenza artificiale. Il 9 ottobre 2023 Tao posta così sui social:

“Ho finalmente deciso di familiarizzare con il sistema di verifica interattivo #Lean4 (ricorrendo all’assistenza dell’intelligenza artificiale, se necessario, per aiutarmi a utilizzarlo)”.

Lean è un assistente di formalizzazione della matematica. Controlla e aiuta nei passaggi delle dimostrazioni (ne abbiamo parlato qui e qui su MaddMaths!). A differenza delle dimostrazioni tradizionali, una dimostrazione formalizzata in Lean deve essere tradotta in una (lunga) sequenza di passaggi logici elementari che il computer può verificare automaticamente. In questo modo non c’è ambiguità. Tuttavia, il processo richiede la scrittura di molto codice. È proprio qui che Tao intravede il potenziale dell’intelligenza artificiale. Sistemi linguistici avanzati possono aiutare a tradurre argomentazioni matematiche nel linguaggio richiesto dai verificatori formali, suggerire passaggi intermedi o individuare percorsi alternativi all’interno di una dimostrazione.

Se Polymath aveva mostrato come una comunità di persone potesse affrontare collettivamente problemi molto complessi, l’intelligenza artificiale potrebbe ampliare ulteriormente questa capacità, partecipando alla soluzione di una miriade di sottoproblemi, agendo direttamente nella dimostrazione. Ecco, nella visione di Tao, l’IA è un ulteriore collaboratore, uno strumento che contribuisce a svolgere compiti specifici all’interno di un processo che resta profondamente umano. Contrariamente a un certo pessimismo, Tao non immagina un futuro popolato da macchine capaci di sostituire i matematici, quanto un ulteriore collaboratore nel processo di nuove scoperte. In quest’ottica di collaborazione tra umani ed IA va anche visto il lavoro di Parisi.

Certo, restano dei limiti. Le macchine non formulano ancora congetture profonde come fanno i matematici e non possiedono quell’intuizione che spesso permette di individuare le domande importanti. Almeno, per ora, non succede in piena autonomia. Tuttavia, secondo Tao, ignorare questi strumenti sarebbe un errore. Il loro contributo potrebbe diventare sempre più significativo nella verifica, nell’organizzazione e nell’esplorazione delle idee matematiche.

In definitiva, l’intelligenza artificiale sta cambiando, e continuerà a farlo, il cosa significa “fare matematica”. Tuttavia, da Erdős a Polymath, fino all’intelligenza artificiale, la matematica resta nella prospettiva di Tao un’impresa umana e di collaborazione. E l’Intelligenza Artificiale non rappresenta una rottura con questa tradizione. Potrebbe invece diventare il prossimo capitolo di una storia che continua ad allargare il numero dei partecipanti a una, almeno per queste righe, delle più grandi avventure intellettuali dell’umanità. Forse, citando ancora Tao, passeremo dai documenti scritti in Latex e condivisi su Overleaf, a un grande linguaggio comune guidato da qualche intelligenza artificiale per ottenere risultati sempre più avanzati. E perché no, forse scopriremo nuove matematiche.