ИИ 5 ноября 2026, 19:16 МСК

AxiomMath заявила о формальной проверке математической библиотеки Stacks Project

AxiomMath сообщила, что её ИИ-агенты перевели около 7654 страниц Stacks Project в 16 млн строк проверенного кода на Lean.

Stacks Project — открытый математический справочник, который Йохан де Йонг начал создавать в 2005 году; он охватывает алгебру, геометрию и теорию чисел. По заявлению AxiomMath, компания формально верифицировала эту библиотеку, сохранив связи между её определениями и теоремами.

Для такой проверки доказательства записывают на языке Lean, после чего программа проверяет их логическую корректность. ИИ-агенты AxiomMath работали параллельно и самостоятельно находили часть задач внутри заданной командой структуры.

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

• Около 7654 страниц математики переведены в код
• Объём формализации — примерно 16 млн строк Lean
• Результат проверки заявлен самой AxiomMath