4 ноября 2026
Axiom выпустила Lean-библиотеку Stacks Project, но ИИ-часть ещё не проверена люд
Axiom 4 ноября выпустила формализацию Stacks Project для Lean поверх Mathlib. Библиотеку можно импортировать в новые доказательства, а связи между утверждениями — смотреть через опубликованный граф зависимостей. По данным компании, релиз охватывает материал справочника объёмом около 7500 страниц и включает примерно 16 млн строк Lean-кода.
Ключевая оговорка — разделение на две зоны доверия. StacksCore уже прошёл человеческую проверку, а StacksFrontier был создан с участием ИИ и пока не завершил такой аудит. При этом Lean машинно проверяет доказательства в обеих частях библиотеки, но это не отменяет риск ошибок в формулировках, предпосылках или переносе исходной математики.
Для команд, которые хотят использовать релиз в рабочих цепочках, это скорее способ ускорить формальную работу, чем готовый источник истины для всех теорем сразу. Всё, что опирается на StacksFrontier в чувствительных сценариях, лучше отдельно отправлять на экспертную проверку.