Il contesto: un’esplosione di soluzioni “AI‑generated” nella matematica

Negli ultimi mesi sembra che l’intelligenza artificiale risolva un nuovo problema matematico ogni settimana. Solo lo scorso mese OpenAI ha pubblicato 719 manoscritti che affermano di aver trovato soluzioni a problemi tra i più difficili del campo. Tuttavia, anche i controlli automatici possono fallire, e dopo anni di “slop” generato dall’AI è lecito chiedersi se la matematica sia il prossimo bersaglio.

AxiomMath scommette che la matematica possa evitare questo destino, non rallentando il progresso, ma fondandosi su un terreno più solido. L’obiettivo della startup da 1,6 miliardi di dollari è costruire una base verificata su cui gli agenti AI possano scrivere software e, in futuro, condurre ricerche scientifiche.

Verifica formale del progetto Stacks

Mercoledì l’azienda ha annunciato di aver verificato formalmente il Stacks Project, uno dei più grandi corpus matematici scritti dall’uomo. Il progetto è così stimato da matematici di spicco: Peter Woit, docente a Columbia, lo ha definito “nulla di comparabile”, paragonandolo ai famosi libri di Bourbaki, che ricostruirono la matematica dalle fondamenta nel XX secolo.

Il collega di Woit, Johan de Jong, avviò il Stacks Project nel 2005 come riferimento open‑source. Da allora, numerosi matematici hanno contribuito, estendendo risultati dall’algebra di base a concetti avanzati di geometria algebrica e teoria dei numeri.

La flotta di agenti AI di AxiomMath ha tradotto le circa 7 654 pagine del progetto in circa 16 milioni di righe di codice controllato da computer.

Che cosa significa “formalizzare” la matematica?

    • Il matematico riscrive la dimostrazione in un linguaggio di programmazione chiamato Lean.
    • Un “proof assistant” verifica il codice riga per riga; se la dimostrazione passa, è logicamente valida.
    • In ingegneria, la stessa tecnica, nota come verifica formale, conferma il corretto funzionamento di circuiti o individua bug in software complessi (ad esempio in programmi francesi per il calcolo di benefici familiari).

Le sfide di un progetto così interconnesso

Per una libreria come Stacks, controllare ogni teorema è solo una parte del lavoro. Teoremi e definizioni sono strettamente collegati: molti risultati tracciano un “albero genealogico” che risale a concetti fondamentali. Questa interconnessione inizialmente ha fatto dubitare Axiom della fattibilità del progetto.

Il team doveva mantenere intatti tutti i collegamenti attraverso circa 16 milioni di righe di codice Lean. “Le cose grandi e delicate nella vita non vanno insieme”, ha dichiarato la CEO Carina Hong a TechCrunch. “Staks è una collezione di risultati matematici che è la base della matematica. Vuoi che i teoremi siano coerenti e non paradossali, le definizioni non si contraddicano.”

Chi c’è dietro AxiomMath?

    • Carina Hong, 25 anni, ha abbandonato un dottorato in matematica a Stanford per fondare la società nel marzo 2025.
    • Nel marzo 2025 Axiom ha raccolto 200 milioni di dollari in Serie A, guidati da Menlo Ventures.
    • Ashvin Swaminathan, membro del team tecnico, ha descritto l’organizzazione del lavoro: “Con Stacks, abbiamo imposto una gerarchia… ma non una gerarchia completa che dettasse cosa fare a ogni singolo agente.”

Strategia operativa: agenti autonomi e modelli addestrati

Per realizzare il progetto, Axiom ha fornito ai suoi agenti una struttura flessibile, lasciandoli operare in parallelo. Gli agenti hanno identificato compiti autonomamente, scegliendo attività che potevano essere svolte simultaneamente.

A differenza di altre startup di verifica, Axiom ha addestrato modelli propri specializzati in matematica. Inizialmente, un esperto interno di Lean ha insegnato agli agenti il “gusto umano” delle dimostrazioni; col tempo gli agenti hanno sviluppato autonomamente questa sensibilità.

Il risultato: colmare il buco nero della matematica formalizzata

Il completamento di Stacks colma una delle più grandi lacune nella matematica formalizzata. “Quando guardi ciò che è stato formalizzato, c’è un enorme buco nero, che copre la geometria algebrica”, ha affermato Swaminathan.

Fino ad ora, i ricercatori che volevano verificare nuovi lavori in geometria algebrica con Lean avevano pochi riferimenti. Ora, grazie a Stacks, hanno una base solida su cui costruire.

Terence Tao, matematico di UCLA e vincitore della Medaglia Fields, ha sintetizzato il concetto: “Più dimostrazioni formalizzate hai, più dimostrazioni formalizzate puoi creare.”

Implicazioni per sviluppatori e futuro del software

Non solo i matematici beneficiano della verifica formale; gli sviluppatori lottano da tempo per garantire che il loro codice sia privo di bug e vulnerabilità. Il problema è accentuato man mano che gli agenti AI scrivono sempre più codice globale.

Axiom scommette che il software del futuro dovrà poggiare su fondamenta verificate, proprio come Stacks ora lo fa per la matematica. “Crediamo che la matematica sia il dominio dove si inizia a costruire queste cose, e che sia una competenza trasferibile”, ha spiegato Swaminathan.

Verso una nuova architettura per l’AI

Il modo in cui gli agenti di Axiom hanno costruito Stacks, lavorando in parallelo e scegliendo autonomamente i compiti, è il modello che Hong prevede per il futuro dell’AI. Gli agenti avranno bisogno di una libreria riutilizzabile per non produrre “slop”.

“Vuoi che gli agenti abbiano una libreria riutilizzabile su cui costruire e spingere il confine”, ha detto Hong. “Se inizi con scelte di ingegneria pessime, è molto difficile far crescere quel confine.”

Confidente, Hong lancia una sfida aperta: “Sfido apertamente tutte le aziende di programmazione a lavorare sulla verifica a questa scala.”