AxiomMath формалізувала Stacks Project для AI
Стартап AxiomMath завершив формальну перевірку Stacks Project і хоче використати цю базу як надійний фундамент для AI-агентів і софту.
AxiomMath оголосила про завершення формальної перевірки Stacks Project — одного з найбільших математичних корпусів, створених людьми. Для стартапу це не лише академічний результат: компанія хоче, щоб на такій перевіреній основі AI-агенти могли писати програмне забезпечення, а згодом допомагати і в науці. На тлі стрімкого потоку AI-контенту питання якості та надійності звучить дедалі гостріше. AxiomMath робить ставку не на уповільнення розвитку ШІ, а на фундамент, якому можна довіряти.
AxiomMath перевела Stacks Project у перевірений код
У середу компанія повідомила, що офіційно formalized, тобто формально перевірила, Stacks Project. Це велика відкрита математична база, яку у 2005 році започаткував Johan de Jong з Columbia University як open-source ресурс.
Відтоді проєкт розширювали математики: від результатів рівня університетської алгебри до складних тем з алгебраїчної геометрії, геометрії та теорії чисел.
За словами AxiomMath, її AI-агенти переклали приблизно 7 654 сторінки бібліотеки у близько 16 мільйонів рядків комп’ютерно перевіреного коду.
Формалізація перевіряє доведення рядок за рядком
Ідея формалізації полягає в тому, щоб перевірити, чи справді математична побудова є логічно бездоганною. Для цього доведення переписують мовою програмування Lean, а спеціальна програма proof assistant перевіряє його рядок за рядком.
Якщо така перевірка проходить успішно, математики отримують більше впевненості, що доказ логічно коректний.
Подібний підхід застосовують і в інших сферах. Інженери використовують formal verification для перевірки роботи чипів, а дослідники у Франції — для пошуку помилок у програмному забезпеченні, яке розраховує сімейні виплати.
Структура Stacks Project стала головною складністю
AxiomMath наголошує, що робота зі Stacks Project була непростою через саму будову бібліотеки. Теореми й означення там тісно пов’язані між собою: одні спираються на інші, майже як у дереві родинних зв’язків.
Саме тому компанія спочатку не була впевнена, що проєкт вдасться довести до кінця. Команді потрібно було зберегти всі зв’язки між матеріалами в межах приблизно 16 мільйонів рядків Lean-коду.
Як повідомляють Новини IT-PUB, CEO AxiomMath Carina Hong сказала TechCrunch, що великі й крихкі речі зазвичай погано поєднуються. Вона назвала Stacks фундаментом математики та підкреслила, що визначення не мають суперечити одне одному й не повинні створювати парадоксів.
AI-агентам дали структуру, але не розписували кожен крок
Щоб реалізувати цей проєкт, команда задала агентам загальну структуру й дозволила працювати паралельно. За словами члена технічної команди Ashvin Swaminathan, AxiomMath не диктувала кожному агенту кожен крок, а вибудувала ієрархію, в межах якої системи самі знаходили собі завдання.
Компанія також навчала власні моделі краще працювати з математикою. Hong сказала, що більшість інших стартапів у сфері верифікації так не роблять. Спочатку команда покладалася на одного внутрішнього Lean-експерта, який допомагав агентам розвивати «чуття» до якості. Згодом, за словами CEO, агенти почали набувати його самостійно.
Hong також визнала, що команда не була впевнена, чи зможе «vibe coding» зберегти цілісність Stacks.
Компанія хоче перенести цей підхід із математики в софт
AxiomMath вважає, що формально перевірені математичні результати можуть стати будівельними блоками для майбутніх систем. Логіка проста: нові доведення зможуть спиратися на вже перевірені, а не починати все з нуля.
Той самий підхід компанія хоче перенести і на програмне забезпечення. Розробники давно намагаються гарантувати, що код не містить помилок і вразливостей, а проблема стає ще гострішою в міру того, як AI-агенти пишуть дедалі більше коду.
AxiomMath робить ставку на те, що майбутнє програмне забезпечення має спиратися на перевірені основи — так само, як тепер це робить Stacks Project.
Swaminathan пояснив, що математика для компанії — це середовище, де можна навчитися будувати такі системи, а потім переносити цей підхід далі. За його словами, Lean-формалізація вже стала основою, на якій агенти можуть будувати нову інфраструктуру.
Hong називає це моделлю майбутньої AI-роботи
Carina Hong вважає, що саме так може працювати значна частина майбутньої AI-роботи: агенти виконуватимуть завдання паралельно й спиратимуться на добре побудовану, багаторазово придатну базу знань.
На її думку, без такої основи AI може генерувати неякісний результат і накопичувати помилки ще на старті. Вона прямо заявила, що якщо закладати погані інженерні рішення з самого початку, то далі розширювати систему буде дуже складно.
Hong також кинула виклик іншим компаніям у сфері розробки, запропонувавши їм працювати над формалізацією в такому ж масштабі. Для ринку це сигнал: змагання в AI може йти не лише за швидкість і гучні демо, а й за якість фундаменту, на якому будуються нові системи.
