Negli stessi giorni in cui l’attenzione globale era concentrata sul CES, un’altra serie di annunci ha scosso in modo forse ancora più profondo le comunità di matematica e intelligenza artificiale. Non si è trattato di nuovi gadget o di modelli più veloci, ma di qualcosa di molto più radicale: la dimostrazione concreta che l’AI sta iniziando a muoversi con sicurezza anche nel territorio più difficile e simbolico della conoscenza umana, quello della matematica pura.
A catalizzare l’attenzione è stata Axiom Math, una startup specializzata in ragionamento matematico automatico, che l’8 gennaio ha annunciato di aver risolto perfettamente tutti e dodici i problemi del Putnam Competition 2025, considerata da molti la competizione matematica universitaria più difficile al mondo. La particolarità non sta solo nel risultato, ma nel modo in cui è stato ottenuto: lo strumento di intelligenza artificiale chiamato AxiomProver ha lavorato in completa autonomia, senza assistenza umana, producendo dimostrazioni formalmente verificate.
Alla base di questo risultato c’è l’uso di Lean, un linguaggio formale che consente di scrivere dimostrazioni matematiche in una forma comprensibile e verificabile da un computer. Quando una dimostrazione viene espressa in Lean, la macchina non si limita a “capirla”, ma ne controlla automaticamente ogni passaggio logico, garantendo che non vi siano errori, salti non giustificati o ambiguità. Il fatto che AxiomProver sia riuscito a risolvere l’intera prova Putnam in questo modo indica che l’AI non solo ha trovato soluzioni corrette, ma è stata in grado di costruire argomentazioni rigorose, snelle e formalmente impeccabili su problemi complessi e non strutturati.
Quasi in parallelo, un altro annuncio ha fatto ancora più rumore, perché ha toccato un territorio che per definizione va oltre le competizioni. Il 7 gennaio, uno studente di matematica dell’Università di Cambridge ha comunicato che GPT-5.2 era riuscito a risolvere autonomamente il problema 728 di Paul Erdős, uno dei famosi problemi aperti lasciati in eredità dal matematico ungherese. Si tratta di una questione di teoria dei numeri legata a condizioni di divisibilità e disuguaglianza sui fattoriali, studiata per anni senza una soluzione definitiva. Per la matematica, i problemi di Erdős non sono esercizi: sono enigmi aperti che definiscono i confini stessi della disciplina.
In questo caso, GPT-5.2 ha generato sia l’idea centrale sia la dimostrazione iniziale. La validazione è poi avvenuta attraverso “Aristotle”, un sistema sviluppato dalla startup Harmonic, che utilizza anch’esso Lean per verificare formalmente la correttezza delle prove. Il ruolo dell’AI, dunque, non si è limitato a suggerire intuizioni, ma ha coperto l’intero arco del ragionamento matematico, dalla formulazione alla verifica.
Poco dopo, un ulteriore tassello ha rafforzato l’impressione di trovarsi davanti a un punto di svolta. Neil Somani, fondatore di Eclipse Labs, ha annunciato di aver dimostrato il problema 397 di Erdős utilizzando GPT-5.2 Pro, con una dimostrazione successivamente confermata da uno dei matematici più autorevoli al mondo, Terence Tao, professore alla UCLA. Non era la prima volta che Harmonic rivendicava un risultato di questo tipo: già lo scorso novembre aveva dichiarato di aver risolto il problema 124 di Erdős, rimasto aperto per quasi trent’anni.
Presi singolarmente, questi episodi sarebbero già notevoli. Considerati insieme, delineano però un quadro molto più ampio: le prestazioni matematiche dei modelli di frontiera stanno crescendo a un ritmo che fino a poco tempo fa sarebbe sembrato irrealistico. Per anni si è discusso del fatto che i large language model fossero bravi a imitare conoscenza esistente, ma deboli quando si trattava di vero ragionamento. Negli ultimi dodici mesi, però, qualcosa è cambiato in modo evidente, soprattutto con l’emergere di una ricerca sistematica sull’inferenza.
Un momento simbolico di questa svolta è stato il successo di OpenAI e Google alle Olimpiadi Internazionali della Matematica nel maggio dello scorso anno. Quelle medaglie d’oro hanno segnato l’inizio di una nuova fase, in cui l’AI non si limita più a riconoscere pattern, ma inizia a costruire catene logiche profonde, affrontando problemi che richiedono astrazione e salti concettuali.
Il confronto tra il Putnam e i problemi di Erdős aiuta a capire la portata del cambiamento. Il Putnam è estremamente difficile, ma resta una competizione con soluzioni note. I problemi di Erdős, invece, sono per definizione territori inesplorati, dove neppure gli esseri umani sanno in anticipo se una soluzione esista o come potrebbe apparire. Il fatto che l’AI riesca a intervenire anche qui suggerisce che non stiamo più parlando solo di rielaborazione di dati di addestramento, ma della capacità di generare nuova conoscenza matematica.
Axiom e Harmonic rappresentano due facce complementari di questa evoluzione. Axiom sottolinea l’eccellenza nella verifica rigorosa delle prove, mentre sistemi come GPT-5.2 e Harmonic mettono l’accento sulla capacità di scoprire le prove stesse. Axiom ha osservato che ciò che è difficile per gli esseri umani non coincide necessariamente con ciò che è difficile per le macchine. Gli umani eccellono nell’intuizione, ma faticano nei compiti ripetitivi e nelle analisi estremamente lunghe; le macchine, al contrario, gestiscono senza problemi enormi spazi combinatori, ma solo ora stanno mostrando una vera capacità di astrazione.
Da qui nasce una visione sempre più concreta della collaborazione uomo-AI. Le macchine possono validare idee in tempo reale, esplorare varianti e bloccare errori, mentre gli esseri umani possono interpretare i risultati, formulare nuove domande e guidare la ricerca verso direzioni promettenti. È la stessa prospettiva espressa da Terence Tao, che già nel 2024 aveva osservato come un uso efficace dell’AI come assistente umano potesse rendere possibile “una scienza su una nuova scala”.
A poco più di un anno di distanza, quella previsione sembra avviarsi a diventare realtà. L’idea astratta di collaborazione uomo-intelligenza artificiale sta prendendo forma concreta, soprattutto in un campo simbolico come la matematica. E proprio per questo, molti vedono in questi risultati segnali sempre più tangibili di ciò che viene chiamato intelligenza artificiale generale, una forma di AI capace non solo di supportare, ma in alcuni casi di superare le scoperte umane.
L’analogia proposta da Axiom è particolarmente efficace: le macchine macinano i chicchi di caffè, gli esseri umani ne assaporano il gusto. In questo equilibrio, l’intelligenza artificiale diventa uno strumento che accelera la ricerca, riduce gli errori e apre nuovi spazi di esplorazione, mentre la creatività, il senso e la direzione restano profondamente umani. Se la matematica è sempre stata il linguaggio ultimo del pensiero rigoroso, il fatto che l’AI stia imparando a parlarlo con sempre maggiore fluidità potrebbe segnare l’inizio di una nuova era per la scienza stessa.