Axiom Math har släppt en maskinverifierad version av Stacks Project, ett viktigt referensverk med öppen källkod inom algebraisk geometri. Formaliseringen översätter projektets matematik till omkring 16 miljoner rader Lean-kod, som ett program för beviskontroll granskar steg för steg. Axiom säger att forskare och AI-agenter kan använda resultaten som ett sammanhängande bibliotek när de tar fram nya formella bevis.
Källorna anger något olika sidantal: TechCrunch rapporterar omkring 7 654 sidor, medan Axiom beskriver projektet som ungefär 7 500 sidor. Det ursprungliga referensverket startades av Columbia-matematikern Johan de Jong 2005 och har byggts ut av matematiker under två decennier. Axioms arbete formaliserar den befintliga forskningen; det innebär inte att AI-agenterna självständigt upptäckte den bakomliggande matematiken.
Varför spelar ett sammanhängande bibliotek roll?
Ett bevisbibliotek är användbart inte bara för att de enskilda satserna har kontrollerats, utan också för att senare bevis kan återanvända dem och deras beroenden. Axiom säger att företaget har bevarat Stacks Projects permanenta taggar, så att Lean-deklarationer länkas till motsvarande delar av originaltexten. På företagets webbplats kan läsare också se texten bredvid koden och undersöka hur resultaten bygger på varandra.
Det är särskilt viktigt inom algebraisk geometri, där ett bevis kan vila på en lång kedja av idéer från områden som kommutativ algebra, scheman, kärvar och kohomologi. Axiom säger att forskare före den här lanseringen hade betydligt mindre Lean-infrastruktur för att formalisera modern algebraisk geometri. Företagets bibliotek ger dem en utgångspunkt, så att de inte behöver formalisera grunderna på nytt för varje projekt.
En grund för framtida bevis – och programvara
Axiom säger att företagets agenter arbetade parallellt med att översätta, bevisa och integrera tusentals satser. TechCrunch rapporterar att företaget gav agenterna en lös struktur, så att de själva kunde hitta uppgifter att arbeta med, och att Axiom även tränade egna modeller med fokus på matematik. Företaget beskriver det färdiga biblioteket som det största integrerade och återanvändbara biblioteket med formaliserad matematik; det är Axioms egen beskrivning av lanseringen.
Samma typ av kontroll används inom områden som chipdesign och programvaruverifiering. Axiom menar att återanvändbara, kontrollerade grunder kan hjälpa AI-agenter att bygga tillförlitligare system i takt med att de skriver mer kod. Men lanseringen verifierar den formaliserade versionen av Stacks Project, inte varje nytt matematiskt påstående eller varje programvara som ett AI-system kan ta fram.
Varför det spelar roll
För matematiker som arbetar med algebraisk geometri erbjuder biblioteket kontrollerade resultat som kan återanvändas, i stället för att bygga upp samma grunder på nytt i Lean. Det bekräftar att detta referensverk har formaliserats, men visar inte att framtida AI-genererade bevis eller kod är tillförlitliga utan kontroll.
