RealFeedApp Axiom выпустила формализацию проекта Stacks из 7500 страниц
Проект Axiom выпустил формализацию Stacks Project в Lean, содержащую около 16 миллионов строк кода. Это крупнейшая библиотека формализованной математики, где теоремы доступны для импорта в новые доказательства исследователями и AI-агентами.
- Область
- программирование
- Что сделали
- Команда Axiom создала формализацию всего проекта Stacks Project (7500 страниц, 16 млн строк кода) в системе Lean, превратив математические доказательства в машинно проверяемую библиотеку.
- Зачем это
- Это позволяет исследователям и агентам ИИ напрямую импортировать определения и теоремы для создания новых формальных доказательств, связывая их с оригинальными текстами математиков.
#lean#mathematics#formalization#ai agents#stacks project
