Axiom Math heeft een machinegecontroleerde versie uitgebracht van het Stacks Project, een belangrijke opensourcereferentie voor de algebraïsche meetkunde. De formalisering zet de wiskunde uit het project om in ongeveer 16 miljoen regels Lean-code, die een programma voor bewijscontrole stap voor stap controleert. Volgens Axiom kunnen onderzoekers en AI-agenten de resultaten gebruiken als één samenhangende bibliotheek om nieuwe formele bewijzen op te bouwen.
De bronnen noemen iets verschillende aantallen pagina’s: TechCrunch spreekt van ongeveer 7.654 pagina’s, terwijl Axiom het project omschrijft als circa 7.500 pagina’s. De oorspronkelijke referentie werd in 2005 opgezet door de wiskundige Johan de Jong van Columbia University en is in de daaropvolgende twintig jaar uitgebreid door wiskundigen. Axioms werk formaliseert dat bestaande wetenschappelijke werk; het betekent niet dat de AI-agenten de onderliggende wiskunde zelfstandig hebben ontdekt.
Waarom is een samenhangende bibliotheek belangrijk?
Een bewijsbibliotheek is niet alleen nuttig omdat afzonderlijke stellingen zijn gecontroleerd, maar ook omdat latere bewijzen die stellingen en hun afhankelijkheden kunnen hergebruiken. Axiom zegt de permanente labels van het Stacks Project te hebben behouden, zodat Lean-definities verwijzen naar de bijbehorende onderdelen van de oorspronkelijke tekst. Op de website kunnen lezers de tekst naast de code bekijken en nagaan hoe resultaten op elkaar voortbouwen.
Dat is vooral van belang in de algebraïsche meetkunde, waar een bewijs kan steunen op een lange keten van ideeën uit vakgebieden als de commutatieve algebra, schema’s, schoven en cohomologie. Volgens Axiom beschikten onderzoekers vóór deze uitgave over veel minder Lean-infrastructuur om moderne algebraïsche meetkunde te formaliseren. De bibliotheek van het bedrijf biedt hun een vertrekpunt, zodat ze die grondslagen niet voor elk project opnieuw hoeven te formaliseren.
Een basis voor toekomstige bewijzen — en software
Volgens Axiom werkten de agenten parallel aan het vertalen, bewijzen en integreren van duizenden stellingen. TechCrunch meldt dat het bedrijf de agenten een globale structuur gaf, zodat ze zelf taken konden identificeren, en dat Axiom ook eigen, op wiskunde gerichte modellen heeft getraind. Het bedrijf noemt de voltooide bibliotheek de grootste geïntegreerde, herbruikbare bibliotheek van geformaliseerde wiskunde; dat is Axioms eigen omschrijving van de uitgave.
Dezelfde soort controle wordt gebruikt op gebieden als chipontwerp en softwareverificatie. Axiom stelt dat herbruikbare, gecontroleerde grondslagen AI-agenten kunnen helpen betrouwbaardere systemen te bouwen naarmate ze meer code schrijven. De uitgave verifieert echter het geformaliseerde Stacks Project, niet elke nieuwe wiskundige bewering of elk stuk software dat een AI-systeem zou kunnen produceren.
Waarom het ertoe doet
Voor wiskundigen in de algebraïsche meetkunde biedt de bibliotheek gecontroleerde resultaten die ze in Lean kunnen hergebruiken, in plaats van dezelfde grondslagen opnieuw op te bouwen. De uitgave bevestigt de formalisering van deze referentie, maar bewijst niet dat toekomstige door AI gegenereerde bewijzen of code betrouwbaar zijn zonder controle.
