Axiom 把 20 年积累的 Stacks Project 形式化进 Lean,可当城市浏览

TheTuringPost · x · 2026-11-12

TheTuring Post 介绍了 Axiom(Carina Hong 团队)为数学家打造的成果:将积累 20 余年的数学参考巨著 Stacks Project 完整形式化为 Lean 形式化证明,并做成可视化——像一座城市,不同街区对应不同数学领域,塔的高度代表依赖层数,点击可看每个定理依赖什么、又被什么使用。

最令人兴奋的点在于协作范式:一个 agent 解决问题时留下的中间成果,可以被另一条证明、另一个人或另一个 agent 复用——Stacks Project 本是数学家代际相传的礼物,现在人机 agent 都能在新证明中取用并把成果留给后来者。