Axiom Math перевела «Проект Stacks» в 16 млн строк верифицированного кода
Стартап Axiom Math объявил о формальной верификации «Проекта Stacks» — одной из крупнейших математических библиотек, созданных людьми. ИИ-агенты компании перевели около 7654 страниц в примерно 16 млн строк кода на языке Lean, который проверяется программой-доказателем.
Что такое «Проект Stacks» и почему это важно
«Проект Stacks» (Stacks Project) — это открытая математическая библиотека, основанная в 2005 году математиком Колумбийского университета Йоханом де Йонгом. С тех пор математики со всего мира пополняли её результатами — от университетской алгебры до передовых идей в алгебре, геометрии и теории чисел.
Библиотека считается уникальной: колумбийский математик Питер Войт сравнивал её с «известными книгами Бурбаки», которые в XX веке перестроили математику с основ. По его словам, «ничего действительно сравнимого» с Stacks нет.
Как проходила верификация
Axiom Math использовала флот ИИ-агентов, которые работали параллельно. Каждый агент самостоятельно находил задачи и проверял логику определений и теорем по всему массиву данных в области алгебраической геометрии. Чтобы сохранить связи между теоремами, команда задала агенту иерархию, но не жёсткую — агенты могли выбирать, что делать.
Компания также обучила собственные модели, специализированные на математике. По словам CEO Axiom Карины Хонг, сначала агентов учил внутренний эксперт по Lean, но со временем они переняли «чувство вкуса» самостоятельно. В результате получилось около 16 млн строк кода на Lean, проверенных построчно программой-доказателем.
Контекст: Axiom Math и формальная верификация
Axiom Math — стартап, основанный в марте 2025 года 25-летней Кариной Хонг, которая бросила аспирантуру по математике в Стэнфорде. В марте компания привлекла $200 млн в раунде Series A под руководством Menlo Ventures, а её оценка составляет $1,6 млрд.
Формальная верификация — это метод, при котором доказательство переписывается на языке программирования (например, Lean) и проверяется программой-доказателем. Такой подход уже применяется в инженерии для проверки чипов и программного обеспечения. Axiom Math считает, что верифицированная математика станет основой для будущих ИИ-систем, которые смогут писать безошибочный код и проводить научные расчёты.
Реакция и планы
Ранее, в октябре, токен Stacks (STX) вырос на 50% за месяц на фоне интереса к стейкингу биткоина, что показывает рост внимания к проектам, связанным с именем Stacks, хотя нынешняя новость относится к математической библиотеке, а не к блокчейн-проекту.
Представители Axiom Math подчёркивают, что верификация Stacks закрывает огромный пробел в формализованной математике, особенно в алгебраической геометрии. Теперь исследователи смогут опираться на проверенные результаты при проверке новых работ. Генеральный директор компании Карина Хонг открыто вызывает все компании, занимающиеся программированием, заняться формализацией в таком масштабе.
Что это значит для пользователей
- Пользователи нейросетей получат более надёжные инструменты для решения математических задач: верифицированная библиотека Stacks может стать основой для ИИ, который не допускает логических ошибок.
- Разработчики смогут использовать проверенный код на Lean для создания безопасного программного обеспечения, особенно в областях, где ошибки недопустимы.
- Компания Axiom Math пока не сообщила, будет ли доступ к результатам бесплатным или платным, и как обычные пользователи смогут их попробовать.
- Стоит учитывать, что формальная верификация требует специальных знаний и пока ориентирована на специалистов; для массового пользователя прямой доступ может быть ограничен.
- По сравнению с существующими инструментами, проект впервые даёт обширную верифицированную базу по алгебраической геометрии, что может ускорить исследования и повысить доверие к ИИ-вычислениям.
Источник: techcrunch.com
Обсудить в Telegram
