AxiomMath оголосила про верифікацію Stacks Project — TechCrunch

Компанія AxiomMath оголосила про формальну верифікацію Stacks Project — великої відкритої бібліотеки математичних результатів. Як повідомляє TechCrunch, її ШІ-агенти переклали приблизно 7 654 сторінки проєкту на близько 16 мільйонів рядків коду Lean, перевіреного комп’ютерним асистентом доказів.

Перевірка математичних доказів

Формалізація математики передбачає переписування доказів мовою програмування Lean. Спеціальна програма — асистент доказів — перевіряє код рядок за рядком. Якщо перевірка проходить успішно, математики можуть вважати доказ логічно коректним.

Stacks Project у 2005 році започаткував математик Колумбійського університету Йоган де Йонг як відкритий довідковий ресурс. Відтоді математики доповнювали його матеріалами — від університетської алгебри до складних тем алгебри, геометрії та теорії чисел. Математик Пітер Войт порівнював значення цього проєкту із серією книжок Бурбакі, що у XX столітті вибудовувала математику з її основ.

Складність роботи полягала не лише у перевірці окремих теорем. Визначення та результати у Stacks Project пов’язані між собою, тому команді потрібно було зберегти всі зв’язки під час роботи приблизно з 16 мільйонами рядків коду Lean.

Більше актуальних новин читайте у Telegram-каналі UA.News.

Основа для нових доказів

Представник технічної команди AxiomMath Ашвін Свамінатан заявив, що результат заповнює велику прогалину у формалізованій математиці, зокрема в алгебраїчній геометрії. За його словами, дослідники, які хочуть перевіряти нові роботи в цій галузі за допомогою Lean, тепер мають базу для такої роботи.

Компанія вважає, що перевірені математичні результати можуть бути повторно використовуваними блоками для нових доказів і основою для інфраструктури, з якою працюватимуть ШІ-агенти. Засновниця та генеральна директорка Каріна Хонг заявила, що агентам потрібна надійна бібліотека знань, аби розвивати її без помилок, закладених невдалими інженерними рішеннями на початкових етапах.

Хонг заснувала компанію у березні 2025 року після того, як залишила докторську програму з математики у Стенфорді. У березні AxiomMath залучила $200 мільйонів у раунді Series A, який очолила Menlo Ventures.