Immagine copertina generata con l’intelligenza artificiale
Le intelligenze artificiali stanno diventando sempre più abili nel risolvere problemi matematici complessi, ma la loro diffusione porta con sé anche una nuova criticità: come distinguere le dimostrazioni corrette da quelle apparentemente convincenti, ma prive di solide fondamenta? È su questo problema che punta a intervenire Axiom Math, startup che ha annunciato di aver completato la verifica formale dello Stacks Project, una delle più importanti raccolte di risultati matematici realizzate dalla comunità scientifica. Un lavoro imponente, che potrebbe offrire agli agenti AI una base di conoscenze controllata sulla quale costruire nuove dimostrazioni, evitando la proliferazione di contenuti matematici non verificati.
L’ascesa dell’intelligenza artificiale nella ricerca matematica
L’intelligenza artificiale sta conquistando uno spazio sempre più importante nella matematica. Gli ultimi sviluppi dimostrano che i modelli possono affrontare problemi particolarmente difficili e contribuire alla produzione di nuove dimostrazioni. Tuttavia, alla crescita delle capacità generative non corrisponde necessariamente un’identica affidabilità dei risultati.
Un esempio citato da TechCrunch riguarda OpenAI, che il mese precedente aveva pubblicato 719 manoscritti contenenti presunte soluzioni ad alcuni dei problemi matematici più difficili. Anche i controlli informatici utilizzati per verificare questi risultati, però, possono presentare delle criticità. Il rischio è quindi quello di trasferire nella ricerca matematica il fenomeno dell’AI slop: una produzione abbondante di contenuti generati automaticamente, ma non sufficientemente controllati.
Axiom Math vuole affrontare questa difficoltà partendo da un presupposto differente: anziché rallentare lo sviluppo degli agenti artificiali, occorre fornire loro una base di conoscenze rigorosamente verificata.
Axiom Math e la sfida della verifica automatizzata
La startup, valutata 1,6 miliardi di dollari, punta a costruire fondamenta matematiche certificate che possano essere utilizzate dagli agenti AI per sviluppare software e, in prospettiva, contribuire alla ricerca scientifica. L’azienda è stata fondata nel marzo 2025 da Carina Hong, amministratrice delegata di 25 anni ed ex dottoranda in matematica a Stanford. Nel marzo 2026 ha inoltre raccolto 200 milioni di dollari in un round di Serie A guidato da Menlo Ventures.
La sua strategia ruota intorno alla verifica formale, una procedura che permette di tradurre le dimostrazioni matematiche in codice, così da sottoporle a controlli automatici. Il linguaggio utilizzato in questo progetto è Lean, affiancato da un programma chiamato proof assistant, che verifica ogni singola riga del codice.
Se il controllo viene superato, la dimostrazione risulta logicamente corretta all’interno del sistema formale. Si tratta di un approccio che non si limita a valutare se una risposta appare plausibile, ma punta a controllarne la coerenza matematica.
La verifica formale dello Stacks Project
Il risultato più significativo raggiunto da Axiom Math riguarda proprio lo Stacks Project, una biblioteca open source avviata nel 2005 dal matematico Johan de Jong della Columbia University. Nel corso degli anni, numerosi ricercatori hanno contribuito ad ampliarla, raccogliendo risultati che spaziano dall’algebra di livello universitario fino agli argomenti più avanzati di algebra, geometria e teoria dei numeri.
La raccolta comprende circa 7.654 pagine e rappresenta un riferimento particolarmente importante per la comunità matematica. Secondo Peter Woit, professore alla Columbia, esistono pochi progetti realmente paragonabili per ampiezza e ambizione.
Per completare la verifica, Axiom Math ha impiegato una flotta di agenti AI, incaricati di trasformare l’intera biblioteca in circa 16 milioni di righe di codice Lean. La difficoltà non consisteva soltanto nel controllare i singoli teoremi: definizioni e dimostrazioni sono infatti strettamente collegate tra loro. Ogni passaggio deve mantenere intatti i rapporti logici con quelli precedenti, senza introdurre contraddizioni.
Nuove prospettive per il controllo delle prove AI
Per affrontare un lavoro di queste dimensioni, Axiom ha organizzato gli agenti secondo una struttura gerarchica, lasciando loro una certa autonomia nell’individuazione delle attività da svolgere. I diversi sistemi hanno potuto lavorare in parallelo, selezionando autonomamente i compiti sui quali intervenire.
Un altro elemento distintivo riguarda l’addestramento: l’azienda ha sviluppato modelli proprietari specializzati nella matematica. Inizialmente, un esperto interno di Lean ha contribuito a trasmettere agli agenti una sorta di sensibilità matematica, che secondo Hong i sistemi hanno progressivamente imparato a sviluppare autonomamente.
Il progetto colma soprattutto una lacuna nell’ambito della geometria algebrica, settore nel quale fino a oggi esistevano poche basi formalizzate utilizzabili dai ricercatori attraverso Lean. La nuova raccolta offre quindi un punto di partenza concreto per verificare ulteriori risultati.
Garantire la qualità della matematica nell’era dell’automazione
L’ambizione di Axiom Math va oltre la ricerca matematica. Una base di conoscenze formalmente verificata potrebbe infatti diventare uno strumento importante anche per gli sviluppatori software, che devono affrontare problemi crescenti legati a bug, vulnerabilità e sicurezza del codice prodotto dagli agenti artificiali.
La società considera la matematica un punto di partenza per costruire infrastrutture riutilizzabili in altri settori. Il principio è semplice: se gli agenti possono leggere e comprendere codice già verificato, possono utilizzarlo per sviluppare nuovi strumenti senza dover ripartire ogni volta da zero.
Verifica e fiducia: il futuro delle dimostrazioni matematiche
La prospettiva è quella di creare un patrimonio di conoscenze che possa crescere progressivamente, permettendo agli agenti AI di costruire nuove dimostrazioni su risultati già controllati. Un concetto che riprende anche una considerazione del matematico Terence Tao, secondo cui più dimostrazioni vengono formalizzate, maggiore diventa la possibilità di formalizzarne altre.
Per Carina Hong, disporre di una biblioteca riutilizzabile è essenziale affinché gli agenti possano continuare ad ampliare le proprie capacità senza accumulare errori nelle fondamenta. La fondatrice ha lanciato anche una sfida alle aziende che sviluppano strumenti di programmazione: investire nella formalizzazione matematica su questa scala. L’obiettivo è evitare che decisioni tecniche sbagliate all’inizio del processo compromettano tutto il lavoro successivo.
Fonte: TechCrunch
