Axiom формализовала в Lean весь Stacks Project — 16 миллионов строк кода
The Stacks Project, Formalized in Lean
Компания Axiom выпустила Lean-формализацию Stacks Project — открытого справочника по алгебраической геометрии объёмом около 7500 страниц. Библиотека насчитывает примерно 16 миллионов строк кода и стала крупнейшей единой переиспользуемой базой формализованной математики. Каждое Lean-утверждение связано с постоянным тегом Stacks, а на stacks.axiommath.ai можно сопоставить исходный текст с кодом и исследовать граф зависимостей. В ходе работы система выявила десятки утверждений, требовавших уточнения, и построила контрпримеры.
В плотно связанном графе зависимостей определений и теорем неверная или тривиализованная формализация быстро выявляется. Убедиться, что каждое формальное утверждение точно передаёт математический смысл исходного текста, даже важнее, чем проверить его доказательство.