Axiom Math zweryfikował Stacks Project z pomocą agentów AI

W ostatnich miesiącach niemal co tydzień pojawiają się doniesienia o kolejnych problemach matematycznych rzekomo rozwiązanych przez sztuczną inteligencję. Tylko OpenAI opublikowało niedawno 719 manuskryptów, które miały zawierać dowody na rozwiązanie najtrudniejszych zagadnień tej dziedziny. Nawet automatyczne kontrole mogą zawodzić. Po latach zalewu niskiej jakości treści generowanych przez AI warto zadać pytanie: czy matematyka podzieli ten los?

Startup Axiom Math stawia na inne podejście. Zamiast zwalniać tempo, firma chce oprzeć się na solidniejszych podstawach. Wyceniane na 1,6 mld dolarów przedsięwzięcie buduje zweryfikowany fundament, na którym agenci AI będą mogli tworzyć oprogramowanie, a w przyszłości prowadzić badania naukowe.

Czym jest Stacks Project i dlaczego ma znaczenie

W środę Axiom Math ogłosił, że udało się formalnie zweryfikować Stacks Project — jedno z najobszerniejszych dzieł matematycznych stworzonych przez ludzi. To projekt o wyjątkowym statusie w środowisku akademickim. Matematyk z Columbia University, Peter Woit, określił go jako przedsięwzięcie niemające sobie równych, porównując je do słynnych książek Bourbakiego, które w XX wieku przebudowały fundamenty tej dyscypliny.

Założycielem Stacks Project jest Johan de Jong, również związany z Columbia University. Prace rozpoczęły się w 2005 roku jako otwartoźródłowe repozytorium wiedzy. Od tego czasu matematycy z całego świata sukcesywnie je rozbudowywali — od podstawowej algebry wykładanej na pierwszym roku studiów, aż po najbardziej zaawansowane koncepcje z zakresu algebry, geometrii i teorii liczb.

Jak agenci AI przekształcili matematykę w kod

Zespół Axiom Math wykorzystał flotę agentów AI do przetłumaczenia biblioteki liczącej około 7654 stron na blisko 16 milionów linii kodu możliwego do automatycznej weryfikacji. Proces ten opiera się na formalizacji matematyki — metodzie, która pozwala upewnić się, że struktura leżąca u podstaw dowodów jest logicznie spójna.

Mechanizm działania jest następujący: matematycy przepisują dowód w języku programowania Lean, a następnie specjalne narzędzie zwane asystentem dowodowym sprawdza kod linia po linii. Jeśli weryfikacja przebiegnie pomyślnie, można mieć pewność, że rozumowanie jest poprawne pod względem logicznym. Inżynierowie stosują tę samą ideę — nazywaną weryfikacją formalną — do potwierdzania działania projektów układów scalonych. Francuscy badacze wykorzystali ją z kolei do wykrywania błędów w oprogramowaniu obliczającym świadczenia rodzinne.

Wyzwanie: zachować wszystkie połączenia

W przypadku biblioteki takiej jak Stacks Project sprawdzenie każdego twierdzenia to zaledwie część zadania. Twierdzenia i definicje są ze sobą wzajemnie powiązane — każde kolejne opiera się na wcześniejszych. Ta sieć zależności przypomina drzewo genealogiczne, w którym wiele wyników wywodzi się z wcześniejszych rezultatów.

Właśnie ta złożoność początkowo budziła wątpliwości zespołu Axiom, czy projekt się powiedzie. Twórcy musieli zadbać o zachowanie wszystkich połączeń w około 16 milionach linii kodu Lean.

„Rzeczy duże i rzeczy delikatne w życiu po prostu do siebie nie pasują. [Stacks] to zbiór wyników matematycznych stanowiących fundament tej dziedziny. Chcesz, żeby [twierdzenia] były spójne, a nie paradoksalne. Chcesz, żeby definicje nie kłóciły się ze sobą” — powiedziała Carina Hong, dyrektorka generalna Axiom, w rozmowie z TechCrunch.

Młoda firma, ambitne plany

Carina Hong ma 25 lat i przerwała studia doktoranckie z matematyki na Stanford University, by w marcu 2025 roku założyć Axiom. W tym samym miesiącu firma pozyskała 200 milionów dolarów w rundzie finansowania Series A, którą poprowadził fundusz Menlo Ventures.

Hong przyznała, że zespół nie miał pewności, czy „vibe coding" — czyli podejście oparte na luźnych wytycznych dla modeli AI — pozwoli zachować matematyczne piękno Stacks. Aby sprostać wyzwaniu, agenci otrzymali ogólną strukturę i mogli działać równolegle.

„W przypadku Stacks narzuciliśmy hierarchię... [ale] nie była to kompletna hierarchia dyktująca każdemu pojedynczemu agentowi, co ma robić" — wyjaśnił Ashvin Swaminathan z zespołu technicznego Axiom. „Agenci sami znajdowali zadania i identyfikowali rzeczy, nad którymi mogli pracować równolegle".

Własne modele i wyczucie matematyczne

Axiom wytrenował również własne modele pod kątem zdolności matematycznych — podejście, które według Hong większość innych startupów zajmujących się weryfikacją pominęła. Początkowo zespół opierał się na wewnętrznym ekspercie od Lean, który uczył agentów ludzkiego wyczucia tego, co w matematyce istotne. Z czasem, jak twierdzi CEO, agenci zaczęli samodzielnie rozwijać tę umiejętność.

Rezultat wypełnia jedną z największych luk w sformalizowanej matematyce. „Kiedy spojrzysz na to, co zostało sformalizowane, widzisz ogromną czarną dziurę. Ta czarna dziura obejmuje geometrię algebraiczną" — powiedział Swaminathan. Do tej pory badacze chcący sprawdzić nowe prace z tej dziedziny przy użyciu Lean mieli niewiele, na czym mogli się oprzeć. Teraz mają solidną bazę.

„Im więcej masz sformalizowanych dowodów, tym więcej sformalizowanych dowodów możesz stworzyć" — stwierdził Terence Tao, matematyk z UCLA i laureat Medalu Fieldsa.

Od matematyki do oprogramowania

Matematycy nie są jedyną grupą docelową Axiom. Programiści od dawna zmagają się z problemem zagwarantowania, że ich kod jest wolny od błędów i luk bezpieczeństwa. To wyzwanie rośnie wraz z tym, jak coraz większa część światowego oprogramowania powstaje przy udziale agentów AI.

Axiom zakłada, że przyszłe oprogramowanie będzie musiało opierać się na zweryfikowanych fundamentach — podobnie jak Stacks Project. Każdy potwierdzony wynik staje się bowiem cegiełką, na której można budować kolejne dowody, zamiast zaczynać od zera.

„Wierzymy, że matematyka jest dziedziną, od której zaczyna się budowanie takich rzeczy, i że jest to umiejętność przenośna" — powiedział Swaminathan. „Agenci mogą czytać nasz kod, rozumieć go i budować nową infrastrukturę na jego podstawie. Nasza formalizacja w Lean jest teraz podłożem, na którym agenci mogą pracować".

Sposób, w jaki agenci Axiom zbudowali Stacks — działając równolegle i samodzielnie wybierając zadania — zdaniem Hong odzwierciedla przyszłość pracy z AI. Jej zdaniem agenci będą potrzebować dobrze zaprojektowanego, wielokrotnego użytku zasobu wiedzy, aby nie generować bezwartościowych treści.

„Chcesz, żeby [agenci] mieli bibliotekę wielokrotnego użytku, na której mogą budować i przesuwać granice" — tłumaczy Hong. „Jeśli na początku popełnisz złe decyzje inżynierskie, bardzo trudno będzie im rozszerzyć tę granicę".

Hong jest wystarczająco pewna swojego podejścia, by rzucić wyzwanie konkurencji. „Otwarcie rzucam wyzwanie wszystkim firmom zajmującym się kodowaniem, aby podjęły się formalizacji na taką skalę" — zadeklarowała.

Projekt Axiom pokazuje, że wyścig o jakość w erze AI może rozgrywać się nie na polu szybkości generowania treści, lecz na polu budowania trwałych, sprawdzalnych fundamentów. Czy inne firmy podejmą rzuconą rękawicę — i czy weryfikacja formalna stanie się nowym standardem także poza matematyką?