Axiom Math ha pubblicato una versione verificata automaticamente dello Stacks Project, un’importante opera di riferimento open source sulla geometria algebrica. La formalizzazione traduce la matematica del progetto in circa 16 milioni di righe di codice Lean, controllate passo dopo passo da un programma di verifica delle dimostrazioni. Secondo Axiom, ricercatori e agenti di IA possono usare i risultati come una libreria interconnessa per costruire nuove dimostrazioni formali.
Le fonti riportano conteggi delle pagine leggermente diversi: TechCrunch parla di circa 7.654 pagine, mentre Axiom descrive il progetto come composto da circa 7.500 pagine. L’opera di riferimento originale è stata avviata nel 2005 dal matematico della Columbia Johan de Jong e ampliata nel corso di due decenni da altri matematici. Il lavoro di Axiom formalizza risultati già esistenti: non significa che gli agenti di IA abbiano scoperto autonomamente la matematica su cui si basano.
Perché è importante avere una libreria interconnessa?
Una libreria di dimostrazioni è utile non solo perché i singoli teoremi sono stati verificati, ma anche perché le dimostrazioni successive possono riutilizzarli, insieme alle loro dipendenze. Axiom afferma di aver mantenuto i tag permanenti dello Stacks Project, collegando le dichiarazioni in Lean alle sezioni corrispondenti del testo originale. Sul sito dell’azienda è inoltre possibile consultare il testo accanto al codice e vedere da quali risultati dipendono gli altri.
Questo è particolarmente importante in geometria algebrica, dove una dimostrazione può basarsi su una lunga catena di idee provenienti da ambiti come l’algebra commutativa, gli schemi, i fasci e la coomologia. Axiom sostiene che, prima di questa pubblicazione, i ricercatori disponevano di strumenti Lean molto più limitati per formalizzare la geometria algebrica moderna. La libreria dell’azienda offre loro un punto di partenza, evitando di dover formalizzare nuovamente quelle basi per ogni progetto.
Una base per le dimostrazioni future e per il software
Secondo Axiom, i suoi agenti hanno lavorato in parallelo per tradurre, dimostrare e integrare migliaia di teoremi. TechCrunch riferisce che l’azienda ha fornito agli agenti una struttura flessibile, lasciando loro individuare le attività da svolgere, e che Axiom ha anche addestrato modelli propri specializzati in matematica. L’azienda definisce la libreria completata la più grande libreria integrata e riutilizzabile di matematica formalizzata: è la descrizione che Axiom dà della propria pubblicazione.
Lo stesso tipo di verifica viene usato in ambiti come la progettazione di chip e la verifica del software. Axiom sostiene che basi verificate e riutilizzabili potrebbero aiutare gli agenti di IA a creare sistemi più affidabili man mano che scrivono più codice. La pubblicazione, però, verifica lo Stacks Project formalizzato, non ogni nuova affermazione matematica o ogni programma che un sistema di IA potrebbe produrre.
Perché conta
Per chi lavora in geometria algebrica, la libreria mette a disposizione risultati verificati che possono essere riutilizzati, senza dover ricostruire in Lean le stesse basi. Conferma la formalizzazione di quest’opera di riferimento, ma non garantisce che future dimostrazioni o codice generati dall’IA siano affidabili senza verifica.
