Evaluată la 1,6 miliarde de dolari, compania are o ambiție de o amploare de neînchipuit: construirea unei baze de date verificate, o "fundamentă de beton" pe care agenții de IA să o poată folosi pentru a scrie software de încredere și, pe termen lung, pentru a face știință autentică. Miercuri, Axiom a anunțat o etapă majoră în această misiune: verificarea formală a Stacks Project, una dintre cele mai masive și respectate corpuri de matematică scrise vreodată de oameni.
Un monument al matematicii moderne, transformat în cod
Pentru cei inițiați, Stacks Project nu este o simplă enciclopedie. Este un efort colaborativ, open-source, pornit în 2005 de matematicianul Johan de Jong de la Columbia University. De-a lungul a aproape două decenii, s-a transformat într-o referință obligatorie, o structură uriașă de aproximativ 7.654 de pagini care acoperă totul, de la algebră de nivel universitar până la vârfurile cele mai avansate ale geometriei algebrice și a teoriei numerelor. Matematicianul Peter Woit, coleg al lui de Jong la Columbia, l-a comparat cu faima serie Bourbaki – acea inițiativă care a reconstruit matematica de la bazele sale în secolul al XX-lea –, spunând că "nu există nimic altceva cu adevărat comparabil".
Dar Axiom Math nu s-a mulțumit cu admirarea. Echipa a transformat acest monument al gândirii umane în aproximativ 16 de milioane de linii de cod verificate de calculator, scrise în limbajul de programare Lean. Acesta este inima verificării formale: matematicienii (sau, în acest caz, agenți de IA antrenați special) rescriu demonstrațiile nu în limbaj natural, ambiguu, ci ca cod sursă. Un program numit asistent de demonstrație (proof assistant) verifică apoi fiecare linie, fiecare pas logic. Dacă codul trece testul, demonstrația este logic ireproșabilă. Nu este o chestiune de opinie, ci una de mecanică pură.
Aceeași metodologie este folosită deja în inginerie de înaltă risc – de la verificarea design-urilor de cipuri la detectarea erorilor în software-ul care calculează alocațiile de buget familial în Franța. Dar aplicarea la o scară aici atinsă de Stacks Project este fără precedent.
Provocarea interconectivității: "Lucrurile mari și cele delicate nu se potrivesc"
Cea mai mare dificultate nu a fost volumul, ci arhitectura. Teoremele și definițiile din Stacks nu sunt insulate; ele formează un graf de dependențe dens, un adevărat "copac genealogic" al ideilor, unde un rezultat avansat se bazează pe zeci, poate sute de predecesori. Dacă o singură definiție de la baza piramidei este defectuoasă, întreaga structură risca să se prăbușească.
"Lucrurile care sunt mari și lucrurile care sunt delicate în viață pur și simplu nu se potrivesc", a declarat Carina Hong, CEO-ul Axiom Math, în vârstă de doar 25 de ani, care a părăsit un doctorat în matematică la Stanford pentru a fonda compania în martie 2025. "Stacks este o colecție de rezultate matematice care constituie fundamenta matematicii. Vrei ca teoremele să fie consistente, nu paradoxale. Vrei ca definițiile să nu se certă între ele."
În martie, Axiom a ridicat o rundă Series A de 200 de milioane de dolari, condusă de Menlo Ventures, o validare puternică a viziunii. Dar banii nu rezolvă problema tehnică fundamentală: cum să coordonezi o armată de agenți de IA să construiască acest turn Babel digital fără să se lovească unii de alții?
"Vibe coding" vs. Ierarhie flexibilă
Hong recunoaște că inițial echipa era sceptică: "Nu erăm siguri dacă vibe coding – acea abordare haotică, intuitivă a codării asistate de IA – ar fi putut să conserve frumusețea și rigurozitatea Stacks". Soluția a fost o hibridă inovatoare. Au impus o ierarhie structurală – un cadru general al dependențelor – dar au lăsat agenții să opereze în paralel, cu o autonomie surprinzătoare.
"Agenții își găseau singuri sarcinile și identificau lucrurile pe care puteau să lucreze simultan", explică Ashvin Swaminathan, membru al echipei tehnice. Nu a fost o dictatură centralizată, ci o orchestrare descentralizată. Mai mult, Axiom a antrenat proprie modele, specializați în matematică, o abordare pe care Hong o consideră unică în peisagul startup-urilor de verificare formală. La început, un expert uman în Lean a "învățat" agenții un simț de "gust" matematic – acea intuire estetică și structurală care separă o demonstrație tehnic corectă de una elegantă, naturală. În timp, agenții au internalizat acest gust.
Umplerea "gaurii negre" a geometriei algebrice
Rezultatul nu este doar un exercițiu de forță brută. El rezolvă o criză concretă a comunității de verificare formală. "Când privești ce a fost formalizat în matematică, există o gaură neagră uriașă. Și acea gaură neagră acoperă geometria algebrică", spune Swaminathan. Până acum, cercetătorii care voiau să verifice noi rezultate în acest domeniu cu Lean aveau puține unde să se sprijine. "Bine, acum au."
Filozofia Axiom este cea a blocurilor de construcție. Fiecare rezultat verificat devine o piesă LEGO de încredere. Viitoarele demonstrații nu trebuie să reînvente roata; ele se pot sprijini pe matematică deja certificată. Aceasta este, în esență, viziunea pe care Terence Tao, matematicianul de la UCLA și câștigător al Medaliei Fields, o susținea de mult timp: "Cu cât ai mai multe demonstrații formalizate, cu atât..." (articolul original se întrerupe aici, dar gândul este clar: crește încrederea și accelerează progresul).
Implicații profunde pentru IA și știință
De ce contează acest lucru dincolo de turnul de ivoire al matematicienilor? Pentru că matematica este limbajul ascuns al lumii noastre tehnologice. Dacă agenții de IA viitori vor scrie codul care conduce avioanele, gestionează rețelele electrice sau descoperă noi medicamente, avem nevoie de o garanție că rațiunarea lor matematică de bază nu halucinează. Axiom Math încearcă să construiască acel strat de încredere (trust layer).
Este o cursă împotriva timpului. Pe măsură ce modelele generative devin mai bune la a imita forma științei, riscul de a înunda literatura academică cu "gunoi" care pare adevărat crește exponențial. Axiom nu încearcă să oprească inundația; își construiește un baraj verificabil. Succesul proiectului Stacks demonstrează că, cel puțin pentru matematică, putem avea ambele: viteza și scala IA-ului, și rigurozitatea absolută a verificării formale.
De ce este important:
Această realizare marchează un punct de cotitură critic în relația dintre inteligența artificială și cunoașterea umană. Nu mai este vorba de IA care încearcă să facă matematică, ci de IA care construiește infrastructura de încredere necesară ca matematica să fie sigură la scară industrială. Verificarea Stacks Project demonstrează că putem tămădui haosul generativ al LLM-urilor prin constrângeri logice stricte, transformând IA dintr-un generator de "slop" într-un inginer de cunoaștere certificată. Pentru viitorul dezvoltării software, a criptografiei, a fizicii și a ingineriei, existența unei baze de date matematice de 16 de milioane de linii verificate nu este doar un succes academic – este un act de siguranță existențială într-o epocă a automatizării rațiunii.
