Axiom Math формалізувала бібліотеку Stacks Project у коді Lean

Стартап Axiom Math заявив про формальну верифікацію Stacks Project — однієї з найбільших математичних бібліотек, створених людьми. Компанія перевела приблизно 7654 сторінки матеріалів проєкту в близько 16 млн рядків коду мовою Lean, який перевіряє спеціальна програма-асистент доведень.

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

Перевірка пов’язаних теорем

Формалізація передбачає запис математичного доведення у вигляді коду, який асистент доведень перевіряє рядок за рядком. У разі успішної перевірки таке доведення вважають логічно коректним. Подібні методи формальної верифікації інженери застосовують, зокрема, для перевірки дизайну мікросхем.

Для Stacks Project завдання полягало не лише у перевірці окремих теорем. Визначення та результати в бібліотеці взаємопов’язані й спираються один на одного, тож Axiom Math мала зберегти ці зв’язки у всьому масиві коду. Генеральна директорка компанії Каріна Хонг сказала, що для фундаментальних математичних результатів важливо, аби теореми були узгодженими, а визначення не суперечили одне одному.

Робота ШІ-агентів

За даними компанії, її ШІ-агенти працювали паралельно: їм задали загальну структуру, але вони самі знаходили частину завдань, які можна виконувати одночасно. Axiom Math також навчала власні моделі для математичних задач. На початковому етапі експерт компанії з Lean допомагав агентам засвоїти підхід до роботи з формалізацією.

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

Axiom Math вважає, що перевірені результати можуть слугувати будівельними блоками для наступних доведень, а в майбутньому — для розробки програмного забезпечення. Компанію заснувала Каріна Хонг у березні 2025 року, а того ж місяця стартап залучив 200 млн доларів у раунді Series A, який очолила Menlo Ventures.