华人AI初创Axiom将代数几何百科转为可验证代码

华人初创公司Axiom Math宣布完成代数几何参考项目Stacks Project的形式化，将其转化为可供Lean定理证明器逐条检验的代码。11月4日，Axiom发布约1575万行代码，虽少于此前有限单群分类定理形式化的逾4000万行，但重点在于建成一套持续更新、相互关联的数学知识体系。Stacks Project由哥伦比亚大学数学家约翰·德容于2005年发起，采用开源协作模式，历经20年、由650余名贡献者推进，已扩展至116章、7600余页，以唯一标签和依赖网络串联定义、引理与定理。Axiom基于Mathlib构建代码库，并调度AI智能体分工编写架构、定义和证明，同时保留人工审核：核心层经人工核验，前沿层可由社区认领、审查后升级。团队还发现原书数十处命题需局部修正，并构造出反例。该进展表明，AI形式化正从验证个别前沿定理转向维护可复用、可追溯的数学基础设施。Lean社区认为，这类成果的价值取决于人类能否基于其继续开展研究；当前瓶颈主要是人工审查，Lean内核可证明每一步推导合规，但无法判断代码是否完全忠实原书含义。因此，相关代码短期内难以并入Mathlib，业内也在探索由AI参与规范审查以缓解队列压力。随着审查机制完善，经过验证的代码库有望成为数学家与AI共同调用的推理底座，推动数学研究、审稿与自动证明走向更高水平的严谨化。