AxiomMath bejelentette, hogy formálisan ellenőrizte a Stacks Projectet, az egyik legnagyobb ember által írt matematikai tudásbázist. A cég szerint a körülbelül 7 654 oldalas könyvtár fordítása és ellenőrzése nagyjából 16 millió sor Lean-kódot eredményezett, amelyet bizonyítássegítők (proof assistants) soronként ellenőriznek.
Mi a Stacks Project és miért jelentős?
A Stacks Projectet Johan de Jong indította 2005-ben, mint nyílt forráskódú referenciaanyag, és azóta számos matematikus járult hozzá. A gyűjtemény a középiskolai és egyetemi algebrai anyagtól kezdve az algebra, geometria és számelmélet legmodernebb eredményeiig terjedő tételeket és definíciókat tartalmaz. Egyes szakértők, például Peter Woit (Columbia University), rendkívüli értékűnek tartják a projektet, hasonlítva azt a 20. században a matematikát alapjaiban újraépítő Bourbaki-könyvekhez.
Hogyan működik a formális ellenőrzés?
A formálisizálás lényege, hogy a matematikai bizonyításokat egy Lean nevű programozási nyelven átírják, majd egy proof assistant futtatása ellenőrzi azokat logikai soronként. Ha a Lean-kód átmegy az ellenőrzésen, a bizonyítás logikailag helyesnek tekinthető. Ugyanezt az elvet használják például hardvertervek formális ellenőrzésénél és szoftverhibák felderítésénél.
Technikai és szervezési kihívások
A Stacks Project különlegessége az egymásra épülő tételek és definíciók hálózata: a könyvtár elemei nagyrészt egymásra támaszkodnak, ezért minden kapcsolatot meg kellett őrizni a Lean-kódban. AxiomMath csapata először bizonytalan volt, hogy ez lehetséges-e; a megoldáshoz több tucat, egymással párhuzamosan dolgozó AI-ügynöket használtak, amelyek hierarchiába rendezett, de nem teljesen központosított feladatkiosztásban dolgoztak.
Ashvin Swaminathan, az Axiom műszaki csapatának tagja elmondta, hogy az ügynökök maguk találták meg a feladatokat és párhuzamosan dolgoztak rajtuk, miközben a csapat megőrizte a szükséges struktúrát. A projekt során AxiomMath saját mesterséges intelligencia modelleket is kiképzett, amelyek különösen matematikai feladatokra optimalizáltak; ez a megközelítés állítólag ritkább más formális ellenőrzéssel foglalkozó startupok körében.
A vezetés és a finanszírozás
AxiomMath vezérigazgatója Carina Hong, aki 25 éves, és aki korábban megszakította Stanfordi matematikai PhD-képzését, a vállalatot 2025 márciusában alapította. Ugyanezen a hónapon a cég 200 millió dolláros Series A befektetést kapott a Menlo Ventures vezetésével. A vállalatot a cikk a körülbelül 1,6 milliárd dolláros értékeléssel jellemzi.
Mire jó ez a formalizáció?
AxiomMath érvelése szerint minden formálisan ellenőrzött eredmény egy új, megbízható építőelemmé válik: a jövőbeni bizonyítások nem a nulláról indulnak, hanem a már leellenőrzött matematikára támaszkodhatnak. Ashvin Swaminathan kiemelte, hogy az algebrai geometria területén korábban nagy hiányosságok voltak a formalizált anyagban, és a Stacks formalizálása ezt a fekete lyukat tölti ki.
A célnak nem csak matematikusok a közönsége: a szoftverfejlesztők is profitálhatnak abból, ha a jövő kódjai ellenőrizhető, megbízható alapokra épülnek, különösen, ha AI-ügynökök egyre nagyobb részt vállalnak a kódírásból.
Jövőkép és kihívás
Carina Hong és a műszaki csapat azt várja, hogy az AI-ügynökök munkája a jövőben is gyakran párhuzamosan és autonóm módon zajlik majd, és az ilyen ügynököknek erős, újrafelhasználható tudáshalmazra lesz szükségük, hogy elkerüljék a „sloppiness”-t, a kezdeti rossz mérnöki döntésekből eredő hibákat. Hong nyilvános kihívást intézett a többi kódolócég felé, hogy dolgozzanak hasonló skálájú formalizáción.
Következmények
A Stacks Project teljes formális ellenőrzése fontos lépés a matematikai formalizáció terén: egy már ellenőrzött, nagy méretű könyvtár megkönnyítheti új eredmények formális bizonyítását, és párhuzamosan hozzájárulhat ahhoz, hogy az AI által írt szoftverek és matematikai munkák megbízhatóbbak legyenek. A hosszabb távú hatás a matematikai kutatás módszertanára és az AI-vezérelt szoftverfejlesztésre egyaránt kiterjedhet.
