AxiomMath объявляет о формализации Stacks Project в Lean

AxiomMath объявляет, что выполнила формальную проверку Stacks Project — авторитетной математической библиотеки. В статье, опубликованной 5 ноября, TechCrunch сообщает, что ИИ-агенты компании перевели около 7 654 её страниц примерно в 16 миллионов строк кода, проверенных компьютером. По данным издания, объявление было сделано в среду.

В основе работы лежит Lean — язык, на котором доказательства переформулируются в код, а затем проверяются системой автоматизированного доказательства. Для библиотеки такого масштаба задача выходит за рамки отдельной проверки каждой теоремы: определения и результаты зависят друг от друга. AxiomMath объясняет, что ей пришлось сохранить эти связи на протяжении всего перевода.

Компания представляет эту формализацию как основу для повторного использования, в частности в алгебраической геометрии. По словам её команды, исследователям, желающим проверять новые работы в этой области, до сих пор было доступно мало базовых наработок в Lean. Агенты компании работали параллельно в рамках иерархической организации, которая предоставляла им определённую свободу в выборе задач.

Потенциальная польза заключается в накоплении проверенных результатов, на которые могли бы опираться другие доказательства. AxiomMath также хочет перенести этот подход на программное обеспечение. Пока это остаётся целью: объявление, о котором сообщает издание, касается математической формализации и само по себе не доказывает, что агенты способны создавать программное обеспечение без дефектов.