Axiom 用 Lean 形式化 Stacks Project

Axiom 于 11 月 4 日发布 Stacks Project 的 Lean 形式化库。原项目由研究人员长期协作维护，覆盖现代代数几何的定义、命题和证明。形式化工作把相关内容写成 Lean 可检查的声明，并将声明关联到原项目的永久标签。

团队说明，形式验证之外还会对重要定义和定理做针对性检查，以确认形式化后的表述与原始数学内容相符。11 月 5 日，TechCrunch 对这项工作做了后续报道。

来源：Axiom · TechCrunch。