Axiom Math формально перевірила Stacks Project за допомогою ШІ-агентів

Axiom Math повідомила, що її ШІ-агенти формально перевірили Stacks Project — велику відкриту математичну бібліотеку, яку Johan de Jong започаткував у 2005 році. Вона містить результати з алгебри, геометрії та теорії чисел, що їх доповнювали математики. Математик із Columbia Peter Woit порівнював значення проєкту з книгами Bourbaki.

Компанія перетворила приблизно 7 654 сторінки бібліотеки на близько 16 мільйонів рядків коду мовою Lean. Програма proof assistant перевіряє код рядок за рядком, щоб підтвердити логічну узгодженість доказів. Для Stacks важливо було не порушити зв’язки між означеннями й теоремами, оскільки багато результатів спираються на попередні елементи бібліотеки.

Генеральна директорка Axiom Carina Hong розповіла, що агенти працювали паралельно в межах загальної ієрархії та самостійно знаходили завдання. Компанія також навчила власні моделі математики. В Axiom вважають, що результат створює основу для формалізації алгебричної геометрії, де раніше було мало матеріалів на Lean. Стартап заснували в березні 2025 року, а в березні він залучив $200 мільйонів у раунді Series A під керівництвом Menlo Ventures. Компанія також розглядає перевірену математику як основу для програмного забезпечення, яке створюватимуть ШІ-агенти.