AxiomMath ha annunciato mercoledì la formalizzazione del Stacks Project, uno dei più ampi corpus di matematica mai scritti da persone. L’operazione ha trasformato circa 7.654 pagine in circa 16 milioni di righe di codice Lean, sottoposte a un controllo automatico. L’obiettivo è costruire una base verificata sulla quale gli agenti AI possano sviluppare software e, in prospettiva, produrre nuova scienza.
La notizia si inserisce in un contesto in cui i sistemi generativi producono sempre più testi matematici, ma non sempre con un livello di affidabilità accettabile. Il mese precedente OpenAI aveva pubblicato 719 manoscritti che presentavano soluzioni a problemi considerati particolarmente difficili. Anche i controlli automatici possono tralasciare errori: una risposta formalmente convincente non equivale, inautomatico, a una dimostrazione corretta.
Il Lean è un linguaggio di programmazione usato per riscrivere dimostrazioni matematiche come codice. Un proof assistant controlla il codice Lean riga per riga e, se la dimostrazione supera la verifica, i matematici possono considerarla logicamente solida. Questo approccio, noto come formal verification, è impiegato anche nel settore ingegneristico per confermare il funzionamento dei chip e in progetti di ricerca in Francia per individuare difetti in software destinato al calcolo delle prestazioni familiari.
Nel caso del Stacks Project, la verifica dei singoli teoremi costituiva soltanto una parte del lavoro. Teoremi e definizioni sono infatti collegati tra loro: ciascun elemento poggia su quelli precedenti, formando una struttura simile a un albero genealogico. Per mantenere intatti questi legami, il team di AxiomMath ha dovuto controllare la coerenza dell’intera base di circa 16 milioni di righe di codice Lean.
«Il Stacks Project è una raccolta di risultati matematici che costituisce la base della matematica e richiede coerenza e compatibilità tra definizioni e teoremi.» Con questa definizione Carina Hong, CEO di AxiomMath, ha spiegato la centralità dell’iniziativa. «Non era certo che il vibe coding potesse preservare la bellezza del Stacks Project.»
Il progetto era stato avviato nel 2005 da Johan de Jong, matematico della Columbia University, come riferimento a sorgente aperto. Da allora, diversi matematici hanno contribuito ad ampliarne i contenuti, partendo dall’algebra di livello universitario fino alle idee più avanzate dell’algebra, della geometria e della teoria dei numeri. La sua reputazione è elevata: il matematico della Columbia Peter Woit lo ha paragonato ai «famosi libri di Bourbaki», una serie che nel Novecento ha ricostruito la matematica a partire dalle sue basi.
Per portare avanti la formalizzazione, AxiomMath ha concesso ai propri agenti una struttura organizzativa non rigida e ha consentito loro di operare in parallelo. «Con il Stacks Project AxiomMath ha imposto una gerarchia, senza stabilire però ogni singola attività di ciascun agente: gli agenti individuavano i compiti e lavoravano in parallelo.» A descrivere questo metodo è Ashvin Swaminathan, membro dello staff tecnico dell’azienda.
L’azienda ha inoltre addestrato modelli propri per la matematica, una scelta che, secondo Hong, non è stata adottata dalla maggior parte delle altre startup dedicate alla verifica. Inizialmente, un esperto interno di Lean si è occupato di trasmettere agli agenti un senso estetico di tipo umano; con il passare del tempo, gli agenti hanno sviluppato autonomamente questo criterio di selezione.
Il risultato colma una delle maggiori lacune della matematica formalizzata. «Nella formalizzazione della matematica esiste un’enorme lacuna che riguarda la geometria algebrica.» «Prima di questo lavoro, i ricercatori che volevano verificare nuovi risultati di geometria algebrica con Lean disponevano di pochissime basi.» Con questa base ora disponibile, i ricercatori possono servirsi di un patrimonio di risultati già controllati.
«Ogni risultato verificato può diventare un blocco riutilizzabile sul quale costruire future dimostrazioni.» La logica è quella di una fondazione cumulativa: le nuove dimostrazioni non ripartono da zero, ma si appoggiano su materiale sottoposto a verifica. Terence Tao, matematico della UCLA e vincitore della Medaglia Fields, ha formulato lo stesso principio in modo sintetico: «The more formalized proofs you have, the more formalized proofs you can make.»
L pubblico di riferimento non si limita ai matematici. Da tempo, gli sviluppatori affrontano il problema di garantire che il proprio codice sia privo di difetti e vulnerabilità, un’esigenza destinata a crescere man mano che gli agenti AI scrivono una quota sempre maggiore del software in uso. AxiomMath punta quindi su un futuro in cui le nuove applicazioni software poggino su fondazioni verificate, come già accade al Stacks Project.
«Crediamo che la matematica sia il dominio in cui si iniziano a costruire queste cose, e che si tratti di una competenza trasferibile», ha aggiunto Swaminathan. Gli agenti, ha spiegato, possono leggere il codice, comprenderlo e costruirvi infrastrutture superiori: la formalizzazione in Lean rappresenta ormai un supporto sul quale è possibile sviluppare nuovi sistemi.
Hong considera il lavoro parallelo e autonomo degli agenti un modello per il futuro dell’AI. Secondo la CEO, gli agenti avranno bisogno di una base di conoscenze ben costruita e riutilizzabile per evitare di generare contenuti di bassa qualità. «Vuoi che gli agenti abbiano una libreria riutilizzabile su cui costruire e spingere oltre il confine», ha detto Hong. «Se all’inizio introduci scelte ingegneristiche sbagliate, sarà molto difficile ampliare quel confine.»
La sua sfida si rivolge direttamente alle aziende di programmazione: «Sfido apertamente tutte le aziende di coding a lavorare sulla formalizzazione a questa scala.»
