AI dostało 16 mln linii matematycznej infrastruktury. Axiom sformalizował Stacks Project
Spis treści
Axiom ogłosił formalizację całego Stacks Project w języku Lean. Oznacza to, że rozbudowana biblioteka współczesnej geometrii algebraicznej została zapisana jako kod, którego poprawność logiczną może sprawdzać komputer. Według firmy projekt obejmuje około 7 500 stron i 16 milionów linii kodu.
To ważny krok w momencie, gdy systemy AI generują matematyczne argumenty szybciej, niż ludzie są w stanie je ręcznie analizować. Axiom chce, aby nowe modele nie budowały kolejnych wyników na przypadkowych fragmentach kodu, lecz korzystały ze wspólnej, sprawdzanej warstwy definicji i twierdzeń.
Stacks Project to nie zwykły podręcznik
Stacks Project powstał jako otwarty podręcznik i materiał referencyjny dotyczący geometrii algebraicznej. Oficjalna strona projektu podaje, że jego historia zaczęła się 5 lipca 2005 roku, a pierwsze publiczne wydanie kodu pojawiło się w 2008 roku. Dziś jest to żywa, współtworzona przez matematyków baza przeznaczona przede wszystkim dla doktorantów i badaczy.
Jej szczególną cechą jest sposób organizacji. Wyniki mają trwałe identyfikatory, a kolejne definicje, lematu i twierdzenia odsyłają do zależności, na których się opierają. Dzięki temu Stacks przypomina bardziej rozwijaną bibliotekę oprogramowania niż książkę czytaną od pierwszej do ostatniej strony.
Co właściwie sprawdza Lean?
Lean jest językiem programowania i asystentem dowodzenia. Matematyk lub narzędzie AI zapisuje w nim definicje oraz kolejne kroki dowodu, a zaufane jądro systemu sprawdza, czy wynik wynika z użytych założeń. Nie jest to automatyczne potwierdzenie każdej intuicji ukrytej w tekście. Nadal trzeba poprawnie opisać sens twierdzenia, ale po formalizacji łatwiej wykryć brakujące założenie, niespójność albo błąd w zależnościach.
Axiom podaje, że w trakcie prac znalazł dziesiątki stwierdzeń wymagających lokalnych poprawek, między innymi brakujących hipotez i przypadków brzegowych. Firma twierdzi, że dla części z nich agenci konstruowali kontrprzykłady, a następnie formalizowali poprawione wersje. To pokazuje, że formalizacja może być także narzędziem audytu istniejącej literatury, a nie tylko przepisywaniem jej do innego języka.
Największa wartość kryje się w zależnościach
W przypadku Stacks Project nie chodzi wyłącznie o liczbę linii kodu. Najtrudniejsze jest zachowanie spójności całej sieci zależności, obejmującej między innymi algebrę przemienną, schematy, snopy i kohomologię. Axiom opisuje pracę agentów jako równoległą, ale koordynowaną na grafie zależności. Dzięki temu przyszły dowód może importować gotowe, sprawdzone elementy zamiast odtwarzać podstawy od zera.
To właśnie odróżnia użyteczną bibliotekę od zbioru niezależnych demonstracji. Lean może zaakceptować dwa poprawne fragmenty kodu, które opisują podobny obiekt w niekompatybilny sposób. Dopiero wspólne interfejsy i stabilne definicje sprawiają, że wyniki da się składać w większe konstrukcje.
Co to oznacza dla programistów?
Formalizacja matematyki jest dla Axiom poligonem doświadczalnym. Firma przekonuje, że ta sama idea może być przydatna przy tworzeniu oprogramowania przez agentów AI: kod powinien opierać się na sprawdzonych komponentach, jasno opisanych zależnościach i testowalnych własnościach. Nie rozwiązuje to problemu błędnych wymagań ani złego projektu, ale ogranicza ryzyko, że kolejne warstwy systemu odziedziczą cichy błąd z początku pracy.
Formalizacja Stacks Project jest niezależnym projektem Axiom, a nie zmianą wprowadzoną bezpośrednio do oryginalnego repozytorium. Sam Stacks Project pozostaje rozwijanym źródłem matematyki pod opieką Johana de Jonga i społeczności współtwórców. Axiom udostępnia formalizację wraz z mapowaniem między oryginalnymi tagami a deklaracjami Lean, więc badacze mogą porównywać oba zapisy.
Źródła
Autor Artykułu
Kamil Rogowski
Kamil Rogowski - to pasjonat technologii i sprzętu komputerowego, który od lat śledzi rozwój PC, podzespołów i gamingu. Na pcarena.pl dzieli się testami, opiniami oraz praktycznymi poradami, pomagając czytelnikom wybrać najlepszy sprzęt do pracy i rozrywki. Jego artykuły łączą wiedzę techniczną z lekkim, przystępnym stylem.