The Pulse
Axiom afferma che la sua formalizzazione in Lean copre l’intero Stacks Project
Axiom afferma di aver pubblicato una formalizzazione in Lean dell’intero Stacks Project, un’opera di riferimento open source per la geometria algebrica che conta circa 7.500 pagine. Secondo l’azienda, la formalizzazione comprende circa 16 m
AI.info Team · Scritto con l’IA · verificato ·
Axiom afferma di aver pubblicato una formalizzazione in Lean di quello che descrive come l’intero Stacks Project, l’opera di riferimento open source per la geometria algebrica moderna che conta circa 7.500 pagine. Secondo Axiom, la formalizzazione comprende circa 16 milioni di righe di codice ed è la più grande libreria integrata e riutilizzabile di matematica formalizzata mai realizzata. Axiom afferma che ricercatori e agenti di IA possono importarne definizioni e teoremi in nuove dimostrazioni formali. Secondo Axiom, tag permanenti di Stacks collegano ogni dichiarazione in Lean al testo canonico.
Axiom afferma che lo Stacks Project, di circa 7.500 pagine, è formalizzato in Lean
Lo Stacks Project è stato avviato nel 2005 dal matematico della Columbia University Johan de Jong. Nel corso di due decenni, centinaia di matematici hanno contribuito con dimostrazioni, esempi e perfezionamenti. Axiom afferma che la sua formalizzazione poggia in egual misura sulle basi poste dalle comunità di Lean e Mathlib e che il progetto è stato possibile solo perché queste comunità hanno trascorso anni a costruire una ricca libreria matematica e le astrazioni necessarie per organizzarla.
Axiom presenta il lavoro pubblicato come un’unica libreria verificata automaticamente. Nel suo resoconto descrive lo Stacks Project come una base per la geometria algebrica, con una lunga catena di prerequisiti che attraversa l’algebra commutativa, gli schemi, i fasci, la coomologia e gli stack algebrici. Axiom afferma che la geometria algebrica moderna era stata molto più difficile da affrontare in questo modo perché non esisteva la corrispondente infrastruttura in Lean. Secondo Axiom, la formalizzazione raccoglie le definizioni e i teoremi del progetto in un’unica base di codice che ricercatori e agenti di IA possono riutilizzare.
Axiom afferma che sciami coordinati di agenti di IA hanno lavorato su un grafo delle dipendenze condiviso
Axiom afferma che formalizzare milioni di righe di matematica verificata è stata una sfida tanto di ingegneria del software quanto matematica. L’azienda ha impiegato sciami coordinati di agenti di IA per tradurre, dimostrare e integrare migliaia di teoremi in parallelo. Axiom afferma di aver progettato un sistema gerarchico di agenti di IA con responsabilità specializzate e rigidi protocolli di coordinamento. Il loro lavoro comprendeva la traduzione degli enunciati, la ricerca in Mathlib di astrazioni già esistenti, la costruzione di dimostrazioni e la risoluzione dei prerequisiti.
Axiom afferma che gli agenti hanno lavorato sul grafo delle dipendenze del progetto, mantenendo allineate tra i capitoli le definizioni, le interfacce delle classi di tipi e le astrazioni matematiche. L’azienda sostiene che dimostrazioni verificate indipendentemente possono comunque essere difficili da combinare se utilizzano definizioni incompatibili o duplicano infrastrutture già presenti in Mathlib. Il materiale pubblicato descrive controlli sulla fedeltà degli enunciati che comprendono verifiche condotte da più agenti, controlli incrociati semantici rispetto al testo sorgente e un requisito rigoroso: le definizioni e i lemmi devono interfacciarsi correttamente con i teoremi che ne dipendono. Axiom afferma inoltre di aver condotto verifiche mirate sulle definizioni fondamentali e sui teoremi più significativi.
Axiom afferma che la sua formalizzazione ha individuato decine di enunciati da perfezionare
Axiom afferma che il suo sistema ha portato alla luce decine di enunciati dello Stacks Project che richiedevano perfezionamenti locali. L’azienda cita ipotesi mancanti, casi limite in caratteristica positiva e affermazioni che non erano valide nell’intera generalità enunciata. I suoi agenti hanno costruito controesempi per mostrare dove gli enunciati originali non erano più validi. Axiom afferma che i suoi agenti hanno individuato con precisione le ipotesi mancanti e formalizzato i teoremi corretti insieme ai controesempi.
Nei casi in cui un lemma di supporto falso creava una lacuna nella dimostrazione di un teorema più profondo, Axiom afferma che gli agenti hanno trovato nella letteratura percorsi alternativi per dimostrare il risultato principale sotto le sue ipotesi originali. Il 27 ottobre 2026, Axiom ha pubblicato una formalizzazione della Classification of Finite Simple Groups, che Axiom descrive come organizzata attorno a un unico teorema di riferimento. Secondo Axiom, il valore dello Stacks Project risiede in migliaia di definizioni, costruzioni e lemmi interconnessi, concepiti per essere riutilizzati in dimostrazioni future.
Axiom afferma che la sua formalizzazione in Lean è un progetto open source indipendente
In un annuncio del 21 ottobre 2026, Johan de Jong ha chiesto che per il momento commenti e pull request generati dall’IA non siano inviati direttamente al repository upstream dello Stacks Project. Axiom afferma che lo Stacks Project resta un testo in evoluzione sotto la cura di Johan de Jong e della sua comunità di collaboratori, mentre la formalizzazione in Lean è un progetto open source indipendente mantenuto da Axiom. L’azienda afferma di conservare la formalizzazione, i controesempi e i perfezionamenti nel proprio repository. Secondo Axiom, i lettori possono consultare il testo originale dello Stacks Project accanto al codice Lean ed esplorare il grafo delle dipendenze su stacks.axiommath.ai.