AxiomMath ogłosiła weryfikację Stacks Project — TechCrunch

Firma AxiomMath ogłosiła formalną weryfikację Stacks Project, dużej otwartej biblioteki wyników matematycznych. Jak informuje TechCrunch, jej agenci AI przetłumaczyli około 7654 stron projektu na około 16 milionów linii kodu Lean zweryfikowanego przez komputerowego asystenta dowodów.

Sprawdzanie dowodów matematycznych

Formalizacja matematyki polega na przepisaniu dowodów w języku programowania Lean. Specjalny program — asystent dowodów — sprawdza kod linia po linii. Jeśli weryfikacja przebiega pomyślnie, matematycy mogą uznać dowód za logicznie poprawny.

Stacks Project został zapoczątkowany w 2005 roku przez Johana de Jonga, matematyka z Uniwersytetu Columbia, jako otwarte źródło referencyjne. Od tego czasu matematycy uzupełniali go materiałami — od algebry uniwersyteckiej po złożone zagadnienia algebry, geometrii i teorii liczb. Matematyk Peter Woit porównywał znaczenie tego projektu do serii książek Bourbakiego, która w XX wieku budowała matematykę od jej podstaw.

Złożoność pracy nie polegała wyłącznie na sprawdzaniu poszczególnych twierdzeń. Definicje i wyniki w Stacks Project są ze sobą powiązane, dlatego zespół musiał zachować wszystkie powiązania podczas pracy z około 16 milionami linii kodu Lean.

Więcej aktualnych wiadomości na kanale UA.News w Telegramie Telegram.

Podstawa dla nowych dowodów

Przedstawiciel zespołu technicznego AxiomMath Ashwin Swaminathan oświadczył, że wynik wypełnia dużą lukę w sformalizowanej matematyce, w szczególności w geometrii algebraicznej. Jak stwierdził, badacze, którzy chcą weryfikować nowe prace w tej dziedzinie za pomocą Lean, mają teraz podstawę do takiej pracy.

Firma uważa, że zweryfikowane wyniki matematyczne mogą być ponownie wykorzystywanymi blokami do nowych dowodów oraz podstawą infrastruktury, z którą będą pracować agenci AI. Założycielka i dyrektor generalna Karina Hong oświadczyła, że agenci potrzebują niezawodnej biblioteki wiedzy, aby rozwijać ją bez błędów wynikających z nieudanych decyzji inżynieryjnych na początkowych etapach.

Hong założyła firmę w marcu 2025 roku po odejściu z programu doktoranckiego z matematyki na Stanfordzie. W marcu AxiomMath pozyskała 200 mln dolarów w rundzie Series A, której przewodził Menlo Ventures.