Quando il miglior matematico del mondo cambia il suo modo di pensare

Immaginate un grande maestro di scacchi che, dopo decenni trascorsi da solo davanti alla scacchiera, si ritrovi all’improvviso con un partner capace di suggerire mosse inedite — talvolta brillanti, talvolta assurde, ma sempre sorprendenti. È più o meno ciò che vive Terence Tao da quando ha integrato l’intelligenza artificiale nella sua pratica quotidiana della matematica. E quando parla Tao, la comunità matematica mondiale tende l’orecchio.
Chi è Terence Tao? In due parole: il matematico vivente più ammirato della sua generazione. Australiano-americano, nato nel 1975, ricevette la medaglia Fields nel 2006 — l’equivalente del premio Nobel per la matematica, assegnato ogni quattro anni a ricercatori sotto i quarant’anni per lavori ritenuti eccezionali. Tao lavora in ambiti diversi come la teoria dei numeri, l’analisi armonica e le equazioni alle derivate parziali. Non è un matematico specializzato in un solo ambito: è qualcuno che attraversa con disarmante facilità i muri tra le discipline.
Da diversi anni è anche una delle voci più autorevoli e articolate sull’integrazione dell’IA nella ricerca matematica. Di recente ha pubblicato una sintesi delle sue esperienze e rilasciato diverse interviste per illustrare nel dettaglio le sue osservazioni. Il quadro che traccia è ben lontano da quello di un entusiasta ingenuo — ma anche da quello di uno scettico refrattario.

L’IA come assistente di ricerca: né oracolo né strumento banale

Per capire che cosa cambia l’IA nel lavoro di un matematico, bisogna prima capire in che cosa consista quel lavoro. Contrariamente a quanto spesso si immagina, un matematico di alto livello non trascorre le sue giornate a calcolare. Cerca strutture, regolarità nascoste, percorsi logici che colleghino tra loro delle verità. Una dimostrazione matematica è una catena di argomenti in cui ogni anello deve essere inconfutabile — basta una sola falla e tutto crolla.
In questo contesto, i grandi modelli di linguaggio — quei sistemi di IA addestrati su immensi corpora testuali e capaci di produrre un linguaggio coerente, come GPT-4 o equivalenti — inizialmente sembravano poco adatti alla matematica. La matematica richiede una precisione assoluta; questi sistemi, invece, sono noti per «allucinare», cioè per produrre affermazioni false con imperturbabile sicurezza.
Eppure Tao riferisce qualcosa d’inatteso: se usati correttamente, questi strumenti possono agire come uno sparring partner intellettuale — un partner di allenamento. Non per convalidare dimostrazioni (non sono affidabili a questo scopo), ma per esplorare rapidamente delle piste, riformulare un problema da una prospettiva diversa o individuare analogie con risultati noti in altri ambiti. Insomma: per accelerare la fase esplorativa, prima ancora che entri in gioco il rigore.

«L’IA non sostituisce la dimostrazione. Ma può cambiare il modo in cui cerchiamo che cosa dimostrare.»

—

Ciò che l’IA fa alla cognizione matematica

Tao diventa davvero affascinante quando parla non dei suoi risultati, ma dei suoi processi mentali. Lavorare regolarmente con strumenti di IA, dice, modifica il modo in cui formuliamo i problemi. Si impara a scomporre una questione complessa in sottoquestioni più precise — perché l’IA risponde meglio a richieste ben mirate che a domande vaghe. Così facendo, si affina il proprio pensiero.

È un fenomeno ben noto nella psicologia cognitiva: lo strumento modella chi lo usa quanto chi lo usa modella lo strumento. La calcolatrice ha cambiato il modo in cui pensiamo al calcolo numerico. I software di geometria dinamica hanno cambiato il modo in cui esploriamo le figure. L’IA generativa sta cambiando il modo in cui esploriamo gli spazi delle possibilità matematiche.

Ma questa trasformazione solleva anche una domanda scomoda: se l’IA suggerisce una direzione di ricerca e il matematico la segue fino a una dimostrazione valida, a chi appartiene l’intuizione? La creatività matematica è ancora interamente umana? Tao non prende posizione — ed è proprio questo a rendere interessante la sua posizione. Non cerca di rassicurare. Osserva.

La dimostrazione formale assistita: un cantiere aperto

Oltre ai grandi modelli di linguaggio, Tao si interessa anche a un’altra famiglia di strumenti: gli assistenti di dimostrazione formale, come Lean o Coq. Questi software permettono di verificare meccanicamente ogni passaggio di una dimostrazione matematica — un po’ come un correttore ortografico, ma per la logica pura. Se un passaggio è falso o incompleto, il sistema lo segnala immediatamente.

Tao ha partecipato a progetti collaborativi che usano questi strumenti, in particolare per formalizzare risultati complessi con l’aiuto di decine di collaboratori online. L’esperienza gli ha mostrato che la formalizzazione costringe a esplicitare ipotesi che di solito si lasciano implicite — e può così rivelare lacune insospettate, persino in dimostrazioni reputate solide.

La posta in gioco a lungo termine è considerevole: se si potesse combinare la capacità esplorativa dei grandi modelli di linguaggio con il rigore garantito dagli assistenti di dimostrazione formale, avremmo uno strumento capace al tempo stesso di proporre piste e di verificarle. Non siamo ancora a quel punto — ma la traiettoria è visibile.

Che cosa cambia per studenti e giovani ricercatori

Per uno studente di matematica o un giovane ricercatore, le implicazioni sono immediate e pratiche. Primo punto: l’IA può essere un tutor disponibile ventiquattr’ore su ventiquattro, capace di spiegare un concetto da dieci prospettive diverse finché una di esse non fa scattare qualcosa. È prezioso, soprattutto quando si esita a disturbare il relatore di tesi per una domanda che sembra «troppo elementare».

Secondo punto, più delicato: il rischio di aggirare lo sforzo cognitivo. Imparare la matematica significa in larga misura imparare a restare bloccati — e a uscirne con le proprie forze. Questo attrito scomodo è il motore dello sviluppo intellettuale. Se l’IA fornisce sistematicamente la via di fuga, può privare chi apprende del beneficio dell’ostacolo. Tao insiste su questo punto: lo strumento deve amplificare il pensiero, non sostituirlo.

Terzo punto: le competenze che contano stanno cambiando. Saper porre le domande giuste a un sistema di IA — ciò che si chiama prompting, l’arte di formulare richieste efficaci — sta diventando una competenza a sé stante. Saper valutare criticamente una risposta generata da un’IA, individuarne gli errori, estrarne ciò che è utile: sono queste le capacità che la formazione matematica dovrà integrare esplicitamente.

Né utopia né distopia

Dal bilancio di Tao emerge un atteggiamento raro nei dibattiti sull’IA: né l’entusiasmo beato che annuncia la fine del lavoro umano, né la resistenza irrigidita che rifiuta di vedere ciò che cambia davvero. In sostanza, dice, la matematica resta un’attività profondamente umana — ma il contesto in cui si svolge sta trasformandosi a una velocità senza precedenti.

La vera domanda non è «L’IA sostituirà i matematici?» — la risposta è no, almeno per tutto ciò che riguarda la creatività, l’intuizione profonda, il senso di ciò che è bello o importante in matematica. La vera domanda è: «Come formare matematici capaci di lavorare con questi strumenti senza diventarne dipendenti?» E a questa domanda nemmeno Terence Tao ha ancora una risposta definitiva. Il che, in un certo senso, rassicura.

Concetti da portare con sé

  • Terence Tao ha ricevuto la medaglia Fields — il «Nobel della matematica» — e usa l’IA nella sua ricerca da anni: se lo fa lui con serietà, il tema merita davvero di essere preso sul serio.
  • L’IA non dimostra al posto del matematico: aiuta a esplorare le piste prima che entri in gioco il rigore — come un GPS che propone itinerari, ma siete voi a guidare.
  • Usare regolarmente l’IA cambia il modo in cui pensiamo i problemi — non solo il modo in cui li risolviamo. Lo strumento modifica il cervello di chi lo usa.
  • Esistono software capaci di verificare ogni passaggio di una dimostrazione matematica come un correttore ortografico verifica ogni parola — e talvolta rivelano falle in dimostrazioni che tutti ritenevano solide.
  • Per gli studenti, il vero pericolo dell’IA in matematica non è barare: è non restare mai bloccati — e quindi non imparare più a sbloccarsi da soli.

Per chi ama la matematica

Una delle applicazioni più rigorose dell’IA in matematica riguarda la verifica formale delle dimostrazioni. In questo contesto, una dimostrazione non è scritta in linguaggio naturale, ma in un linguaggio formale compreso da un software — per esempio Lean 4. Ogni passaggio della dimostrazione è un’istruzione che il sistema verifica meccanicamente secondo le regole della logica e gli assiomi scelti (in genere quelli della teoria dei tipi dipendenti o della teoria degli insiemi di Zermelo-Fraenkel). Tao ha contribuito al progetto Polynomial Freiman-Ruzsa (PFR), nel quale una complessa dimostrazione combinatoria è stata interamente formalizzata in Lean in poche settimane grazie a una collaborazione distribuita. L’aspetto matematicamente notevole è che la formalizzazione ha costretto gli autori a esplicitare lemmi intermedi impliciti nella dimostrazione originale, rivelando la struttura fine del ragionamento. A lungo termine, la posta in gioco è integrare questi assistenti di dimostrazione con modelli di linguaggio capaci di generare possibili dimostrazioni — ciò che alcuni chiamano autoformalization: la traduzione automatica di enunciati in linguaggio naturale in dimostrazioni formali verificabili.
Fonte: articolo in tedesco su Der Standard