Il 29 ottobre 2026 Noema ha pubblicato A New Dawn For Mathematical Progress di Atoosa Kasirzadeh, filosofa e matematica, ricercatrice di DeepMind e docente alla Carnegie Mellon University. Il punto di partenza sono i risultati degli ultimi mesi. Il 4 settembre Anthropic ha annunciato la formalizzazione completa in Lean dell’ultimo teorema di Fermat, prodotta da agenti Claude in undici giorni. Poi sono arrivati la singolarità di Navier-Stokes dell’8 settembre, i 722 manoscritti del 6 ottobre e gli annunci del 26 ottobre, fra cui la confutazione dell’ETH. Kasirzadeh scrive che quel giorno è caduto un altro problema del millennio. L’annuncio di OpenAI rivendica però solo l’esistenza della teoria di Yang-Mills, che è una parte del problema, senza il mass gap.

Due modelli di progresso

Kasirzadeh chiama il primo modello checklist. Il progresso consiste nello spuntare una lista di problemi fissati in anticipo: le Olimpiadi della matematica, l’ultimo teorema di Fermat, i cento teoremi da formalizzare raccolti da Freek Wiedijk, i problemi del millennio del Clay Mathematics Institute. Il merito va a chi spunta per primo. È la stessa logica dei benchmark dell’AI ed è il terreno su cui i modelli avanzano più in fretta. Terence Tao parla di un’epoca di proof post-scarcity, in cui le dimostrazioni smettono di essere una risorsa scarsa.

Il secondo è l’incontro generativo: la matematica avanza quando incontra un problema reale che non sta su nessuna lista e ne ricava strutture nuove. Gli esempi del saggio sono due.

  • George Dantzig, dopo il dottorato a Berkeley, ha lavorato per l’aviazione statunitense alla pianificazione della logistica militare, fatta a mano da migliaia di impiegati. Per descriverla ha formulato la programmazione lineare, con un nome preso dal gergo militare, dove programma voleva dire piano: un obiettivo lineare e un insieme di vincoli lineari, che insieme definiscono un poliedro convesso con la soluzione ottima su un vertice. Il metodo del simplesso cerca quel vertice spostandosi lungo gli spigoli. Quando le risorse dovevano essere unità intere, aerei o piloti, dalla stessa strada è nata la programmazione intera.
  • Norbert Wiener, al MIT, è partito da un problema di contraerea: dove mirare quando il pilota cambia rotta. Ha trattato pilota, aereo e cannone come un unico sistema con retroazioni e ne ha ricavato la teoria della predizione e del filtraggio statistico, poi la cibernetica del 1948. Il suo predittore ha avuto poca diffusione: il contratto militare è andato a un progetto più semplice dei Bell Labs. La matematica che ne è uscita è rimasta.

Kasirzadeh aggiunge che la gerarchia fra matematica pura e applicata è un pregiudizio culturale che l’AI costringe a correggere. Lo diceva già Dantzig in un’intervista ripresa nel saggio: “Mathematicians are snobs.”

Quattro campi aperti

Secondo Kasirzadeh il lavoro urgente sta in quattro gruppi di problemi che non compaiono su nessuna lista:

  • infrastrutture informatiche dimostrabilmente sicure;
  • una scienza matematica del deep learning, ancora agli inizi;
  • la matematica del controllo di sistemi multi-agente, con sicurezza, progettazione di meccanismi e teoria dei giochi;
  • l’epistemologia delle dimostrazioni generate dalle macchine, quando sono troppo lunghe o troppo estranee per essere capite.

Propone di spostare la domanda da «chi l’ha dimostrato?» a «chi ha deciso che valeva la pena dimostrarlo, perché e come ci siamo assicurati che fosse corretto?». In chiusura si chiede che cosa succederebbe se un sistema arrivasse a decidere anche quali domande contano e lascia la domanda aperta.

Cosa ne penso

Mi ritrovo nella domanda di Kasirzadeh perché è quella che faccio per i sistemi di AI in generale. Quando produrre risposte costa poco, il lavoro si sposta su quali domande porre e su come verificare le risposte. È quello che intendo per parte umana di una superintelligenza governata. Credo che valga anche per la domanda con cui il saggio si chiude: tenere le persone dentro il sistema, nel punto in cui si decide che cosa conta.

Sulla verifica aggiungerei una distinzione. Il kernel di Lean, il piccolo programma che controlla ogni passaggio, certifica che la dimostrazione è corretta rispetto all’enunciato, non che l’enunciato sia quello giusto. Per Fermat la corrispondenza è stata controllata con un confronto automatico rispetto all’enunciato già presente in Mathlib, la libreria scritta e rivista dalla comunità. Ne avevo parlato per le dieci dimostrazioni certificate di agosto. Decidere che cosa formalizzare e controllare che la formalizzazione dica quello che intendiamo resta lavoro umano. È il quarto campo indicato da Kasirzadeh.

Il primo e il terzo campo sono vicini al lavoro che faccio ogni giorno, la sicurezza delle infrastrutture e il controllo di agenti che interagiscono fra loro. In sanità, in sicurezza e nella pubblica amministrazione i problemi arrivano come quelli di Dantzig, con vincoli che nessuno ha ancora scritto in forma matematica. Credo che sia lì che matematici e modelli possano lavorare meglio insieme. Nella matematica il rigore non ha mai frenato la creatività.

Immagine di copertina: gli ominidi e il monolite della sequenza «L’alba dell’uomo» di «2001: Odissea nello spazio» (Stanley Kubrick, 1968), ricostruiti al Museo de Cine Colin Arthur. Foto di MiguelAlanCS su Wikimedia Commons — CC BY-SA 4.0 — https://commons.wikimedia.org/wiki/File:Museo_de_Cine_Colin_Arthur_11_-_2001_A_Space_Odyssey.jpg — licenza: https://creativecommons.org/licenses/by-sa/4.0/