Gifted, il dono del talento. Un parallelismo tra la storia del talento di Mary e il futuro della matematica.

Tra IA, database di teoremi e normalizzazione della verità

Ho appena visto il film Gifted, e nel ricordo di un articolo di Simone Severini (scienziato attivo nel campo della fisica quantistica e dell’informatica quantistica), si possono azzardare alcune connessioni tra i temi centrali di Gifted e le riflessioni di chi, come Severini, ragiona sul futuro della matematica e della scienza.

Gifted – Il dono del talento (2017), diretto da Marc Webb, racconta la storia di Mary Adler (interpretata da Mckenna Grace), bambina prodigio in matematica affidata alle cure dello zio Frank (Chris Evans) dopo la morte della madre, Diane. Il conflitto centrale ruota attorno al problema di Navier-Stokes, uno dei Millennium Prize Problems del Clay Mathematics Institute-CMI. Diane, ossessionata da questa sfida, finisce per sacrificare la propria salute mentale, lasciando un’enorme eredità intellettuale — ma anche un fardello — alla figlia Mary. Da un lato, Frank cerca di garantire alla nipote un’infanzia il più possibile “normale”; dall’altro, la nonna Evelyn vorrebbe incanalarne il talento esclusivamente verso l’ambita risoluzione del famoso problema sui fluidi.

Nel film, quindi, l’equilibrio fra il genio individuale e la vita comune diventa un tema cruciale. Questa dialettica riflette in modo sorprendentemente accurato alcuni dibattiti che oggi investono la comunità matematica: la necessità di condividere e standardizzare la conoscenza attraverso database di teoremi, l’ingresso dell’IA nel processo di ricerca e il ruolo della creatività umana in un’epoca di automazione

Una sfida dal forte impatto simbolico
il problema Navier-Stokes

Le equazioni di Navier-Stokes, da cui deriva il problema di esistenza e regolarità (“smoothness”), descrivono il moto dei fluidi e vengono utilizzate per prevedere fenomeni fisici che spaziano dalle correnti oceaniche alle dinamiche atmosferiche. Tuttavia, nessuno è ancora riuscito a dimostrare rigorosamente se esistano, per ogni possibile situazione, soluzioni esenti da “singolarità” in tre dimensioni. Il CMI ha messo in palio 1 milione di dollari per chi fornisse la prova definitiva, nella speranza di generare un balzo in avanti nella comprensione dei modelli fluidodinamici.

Nel film, la risoluzione (o tentata risoluzione) di questo enigma diventa il simbolo perfetto di un talento che “consuma” chi lo possiede: Diane si logora nel tentativo di trovare la chiave, e Mary rischia di ripercorrere le stesse orme. Gifted dipinge così un ritratto intenso di come un unico problema possa monopolizzare una vita intera, in parallelo a quanto accade nel mondo reale, dove ricercatori di tutto il pianeta tentano — spesso in solitudine — di svelare i misteri delle equazioni di Navier-Stokes.

La matematica come patrimonio collettivo
verso i database di teoremi

Se l’ossessione di Diane mostra il lato “tragico” della ricerca isolata, la realtà accademica oggi procede — almeno in parte — su un binario differente: la collaborazione e la condivisione di risultati stanno acquisendo sempre più importanza. Come sottolineano diversi matematici (tra cui Terence Tao), la fiducia e il lavoro di squadra rendono possibili progetti estesi su scala mondiale. Tuttavia, l’aumento vertiginoso delle pubblicazioni (oltre 100.000 articoli in un solo anno, secondo MathSciNet) crea un vero e proprio oceano di conoscenza difficile da navigare.

Da qui l’idea di costruire enormi database di teoremi, in cui ogni risultato sia etichettato in modo univoco e verificabile, sia dagli esseri umani sia dalle macchine. L’ispirazione affonda le radici nel Progetto Bourbaki, avviato negli anni ’30 da un gruppo di matematici francesi con l’obiettivo di “riscrivere” la matematica in modo rigoroso e sistematico. Ma l’innovazione attuale mira a normalizzare la verità matematica, non più soltanto a pubblicarla.

Strumenti come il Lean proof assistant e la sua libreria Mathlib vanno proprio in questa direzione. Formalizzare un teorema in Lean significa tradurlo in un linguaggio che il computer possa comprendere e verificare, rendendolo parte di un gigantesco archivio di conoscenze interconnesse. Questo offre due vantaggi cruciali:

1. Affidabilità e correttezza
   il sistema impedisce che errori o passaggi scorretti passino inosservati, poiché ogni step deve essere rigorosamente giustificato.
2. Collaborazione su larga scala
   i matematici di ogni parte del mondo possono contribuire all’ampliamento di Mathlib, sapendo che il computer garantirà la coerenza dell’insieme.

In Gifted, vediamo come la solitudine di una singola mente geniale possa diventare deleteria. Per contrasto, un database di teoremi verificati dalla macchina favorisce esattamente l’opposto: costruire la matematica come un patrimonio collettivo, in cui chiunque possa cimentarsi nella risoluzione di problemi partendo da fondamenta solide.

La rivoluzione dell’IA
da Undermind a LeanDojo

Parallelamente, nuovi strumenti IA come Undermind mostrano come l’uso intelligente di un modello linguistico possa rivoluzionare la ricerca accademica. Undermind funge da “assistente umano esperto”, in grado di comprendere query complesse e navigare tra milioni di articoli, fornendo non solo un elenco di fonti, ma anche spiegazioni approfondite dei risultati. Se un progetto del genere potesse agganciarsi a un database di teoremi formale, la letteratura verrebbe trasformata in un sistema “vivo” e interattivo, in cui è più semplice distinguere tra verità matematiche consolidate e speculazioni ancora da validare.

In un contesto ancora più specializzato, progetti come LeanDojo (nati a Caltech) puntano invece ad automatizzare parte del processo di dimostrazione e ricerca all’interno di Lean. Attraverso l’apprendimento automatico e i large language model (LLM), questi sistemi tentano di suggerire o completare interi passaggi logici, trasformandosi in veri e propri copiloti per i matematici.

Tuttavia, come emerge dal film, la vera sfida sta nel mantenere un equilibrio tra l’assistenza che fornisce la tecnologia e la creatività umana. Se da un lato l’automazione può produrre valanghe di risultati o “verità”, dall’altro è fondamentale che i ricercatori conservino la capacità di porsi nuove domande, di sviluppare intuizioni inaspettate e di mettere in discussione lo status quo.

Oltre la verifica
la nascita di nuove congetture

Il tema della creatività ritorna spesso nel dibattito sull’IA. Gifted offre una metafora potente su questo argomento: Mary possiede un dono ineguagliabile, ma nel corso del film capisce di volerlo impiegare in modo che non la alieni dal resto del mondo. Allo stesso modo, le macchine possono verificare le nostre dimostrazioni o persino suggerire teoremi, ma la scintilla dell’intuizione umana rimane un aspetto insostituibile.

Le nuove frontiere, come la “superintelligenza matematica” teorizzata da alcuni (si pensi a progetti come ad esempio Harmonic, Isabelle, Coq) suggeriscono un futuro in cui l’IA potrebbe arrivare a formulare da sé nuove congetture, facendo domande che non ci siamo mai posti. Un computer che non si limita a “dare risposte”, ma che sa porre interrogativi dirompenti, aprirebbe scenari ancora inediti. Eppure, le emozioni, le esperienze di vita e l’intuizione romantica di un ricercatore resterebbero ingredienti fondamentali: la macchina non si distrae, non “sogna” di trasformare un’idea in una canzone, non fa analogie bizzarre guardando la luna. Spesso è proprio in questi momenti di apparente “vaga” creatività che sorgono spunti determinanti per avanzare in matematica.

Normalizzazione della verità
rischi ed opportunità

Un grande archivio di teoremi e dimostrazioni formali offre innumerevoli vantaggi, ma non è privo di rischi:

• Diluzione e rumore
  Un database monolitico, se non gestito correttamente, rischia di accumulare risultati banali o duplicati, confondendo le scoperte realmente rilevanti.
• Perdita di diversità
  La matematica vive anche di approcci non convenzionali. Monolitismo e uniformità potrebbero appiattire la creatività, soffocando idee fuori dagli schemi.
• Barriere di accesso
  Formalizzare teoremi in Lean richiede competenze di programmazione e tempo. Se questo sforzo non viene semplificato o reso graduale (attraverso l’autoformalizzazione e l’autoinformalizzazione), si rischia di escludere chi non dispone delle risorse o della formazione adeguata.

Tuttavia, queste problematiche non annullano il valore della normalizzazione della verità. Al contrario, spingono la comunità scientifica a trovare soluzioni responsabili, come la creazione di procedure di controllo qualità (ad esempio, revisori umani e software di verifica automatica) e strumenti che semplifichino l’interazione tra linguaggio informale e formale. Se gestito correttamente, un grande database di teoremi potrebbe concretizzare la “democratizzazione” (o “normalizzazione”) della conoscenza, permettendo a chiunque — anche a un giovane talento come Mary in Gifted — di contribuire e verificare la propria parte di verità.

In un futuro iperconnesso

La storia di Mary Adler mette in scena la tensione fra un dono straordinario e la necessità di una vita “vera”, fatta di rapporti umani, passioni e momenti di serenità. Questo aspetto è intimamente legato al futuro della matematica. Se strumenti come Lean, Undermind, LeanDojo e altri proof assistant o motori di ricerca specializzati promettono di trasformare la ricerca in un’impresa collettiva, resta vitale la fiamma dell’iniziativa personale, quella “strana creatività” che talvolta scaturisce da un’intuizione fuori contesto o dalla semplice curiosità.

In fondo, Gifted ci ricorda che la matematica non è soltanto un insieme di regole e dimostrazioni: è anche uno spazio umano, dove talento e dedizione possono portare a grandi scoperte, ma anche a un doloroso isolamento se non si trova un equilibrio. L’IA e i database di teoremi renderanno la matematica più accessibile, veloce e collaborativa, ma dovremo essere abili nel preservare l’inventiva, l’ironia, la bellezza e il senso di meraviglia di cui i matematici — e gli appassionati di ogni età — si nutrono fin dai tempi di Pitagora e Archimede.

Come direbbe Mary, la meraviglia più grande non è solo risolvere un problema complicato, ma anche vedere come la soluzione si inserisce in un gioco di specchi fatto di altre verità e persone. Uno specchio infinito, dove ogni teorema acquisisce valore nel riflesso di ciò che ancora non sappiamo. E chissà, forse un giorno, in un ipotetico database universale, troveremo davvero la dimostrazione definitiva del problema di Navier-Stokes. Ma quella, come insegna Gifted, sarà solo una tappa del viaggio umano e collettivo alla scoperta di nuovi orizzonti matematici.

Il contributo di Simone Severini
normalizzazione della verità e AI

Proprio sul tema della normalizzazione della verità e della creazione di database formali, Simone Severini offre spunti interessanti. Nel film, la madre di Mary dedica la vita al problema di Navier-Stokes, per poi lasciarne l’eredità alla figlia. Questo suggerisce la sfida di custodire e tramandare scoperte e “verità” matematiche. Nello scenario attuale, caratterizzato da una produzione scientifica vertiginosa, Severini e altri scienziati riflettono sulla necessità di rendere i teoremi verificabili e ricercabili in modo automatizzato, così da garantire trasparenza e affidabilità.

Equilibrio tra genio individuale e sforzo collettivo

Come sottolineato anche da Terence Tao, la ricerca isolata del “genio solitario” può essere controproducente di fronte a problemi estremamente complessi. Nel film, ciò si riflette nel conflitto tra lo zio Frank e la nonna Evelyn: il primo vuole regalare a Mary la semplicità di un’infanzia serena, la seconda pensa che la bambina debba seguire un “mito matematico” più grande di lei. Nella realtà, Severini e molti altri studiosi suggeriscono che la strada maestra sia la collaborazione, sia umana sia con l’ausilio dell’IA.

AI e “superintelligenza matematica”

L’articolo di Severini tocca infatti anche il tema dell’intelligenza artificiale applicata alla ricerca in matematica e fisica quantistica. Se in Gifted Diane e Mary sognano di risolvere Navier-Stokes con la sola forza della propria mente, oggi intravediamo la possibilità di una collaborazione uomo-macchina. Sistemi come Undermind o LeanDojo riorganizzano la letteratura scientifica e suggeriscono nuove linee di indagine, alleggerendo così il fardello del ricercatore.

Sorge spontaneo chiedersi: se Mary avesse avuto accesso a questi strumenti fin dalla prima infanzia, avrebbe vissuto la stessa ossessione della madre? O magari avrebbe sviluppato un percorso più armonioso, fatto di creatività umana e aiuto tecnologico? Non c’è risposta semplice, ma la questione solleva riflessioni su come preservare la creatività e l’intuizione in un contesto altamente automatizzato.

Rischi e potenzialità di una “Gifted society”

1. Rischio di isolamento
   Nel film, l’isolamento di Mary e soprattutto della madre Diane rappresenta una condizione estrema. Sul piano tecnologico, l’adozione massiccia di IA e di database formali potrebbe escludere chi non ha i mezzi o le competenze per usarli, creando nuove forme di solitudine digitale.
2. Condivisione del sapere
   Un sistema ben progettato, aperto e fruibile — come suggerito da Severini — potrebbe invece accelerare lo scambio di risultati, favorendo la normalizzazione della verità in matematica, ossia la creazione di un corpus di conoscenze più solido e accessibile a tutti.
3. Creatività e nuove domande
   Non è soltanto importante trovare risposte, ma anche porre nuove domande. Se Mary avesse avuto accesso, sin da bambina, a un’immensa banca dati di teoremi, avrebbe forse fatto domande diverse rispetto a quelle di sua madre, arrivando a soluzioni innovative o a congetture completamente nuove.

Concludendo, l’azzardato parallelismo tra il film Gifted e le riflessioni di uno studioso come Simone Severini evidenzia come la vicenda di Mary Adler non sia solo una parabola sul talento individuale, ma anche uno specchio delle sfide reali che la matematica e la scienza affrontano oggi. Da una parte, il film mostra la dimensione umana: le emozioni, i rapporti familiari, il sacrificio e la pressione sociale che accompagnano un genio precoce. Dall’altra, gli articoli di Severini richiamano l’innovazione tecnologica, la costruzione di banche dati condivise e i grandi progetti di IA per la formalizzazione delle conoscenze.

Entrambi i livelli — il lato umano e quello tecnologico — emergono come fondamentali per il futuro della ricerca. L’importante, come ricorda la storia di Mary, è non dimenticare mai che dietro ogni teorema e ogni soluzione c’è una mente (o un gruppo di menti) con passioni, ricordi, speranze e, talvolta, fragilità. In definitiva, è la giusta commistione tra cuore e rigore, tra curiosità e sistematicità, a rendere la matematica (e la vita) un’avventura sorprendente.

E, forse, la più grande lezione di Gifted è proprio questa: non importa quanto avanzati diventino i nostri strumenti — IA, database di teoremi, superintelligenze matematiche — il mistero e la meraviglia della scoperta rimangono profondamente umani. Ecco perché, come dice Mary, la vera magia non sta solo nel risolvere un problema, ma anche nel condividerne il percorso e nel continuare a fare domande.