Axiom Math 正式使用 AI 智能体验证了 Stacks Project
Axiom Math wants to keep AI slop out of mathematics
- 谁
- Axiom Math
- 引文
On Wednesday, the company announced it had formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans.
发生了什么
Axiom Math 表示，该公司已对 Stacks Project 进行形式化验证。Stacks Project 是一本开放源码的数学参考资料，由 Johan de Jong 于 2005 年创立。该公司的智能体将约 7,654 页内容转译为约 1,600 万行 Lean 代码，并由证明助手逐行检查。Axiom 表示，经过验证的结果为研究人员在代数几何领域开展后续工作奠定了基础，也可能为 AI 智能体构建的软件提供支持。
推荐理由
Axiom 对 Stacks Project 的形式化工作展示了如何将大型、相互关联的数学库转化为经过检查的基础，以支持后续证明和由智能体构建的软件。
接下来读什么
查看这件事的完整进展Axiom Math Says Its AI Agents Formally Verified the Stacks Project这件事到目前为止
Axiom Math says its agents formally verified the Stacks Project, an open-source mathematics reference founded by Johan de Jong in 2005. The company says they translated about 7,654 pages into roughly 16 million lines of Lean code, which a proof assistant checked line by line. Axiom says the verified results could give researchers a foundation for future work in algebraic geometry and support software built by AI agents.
每天一封，跟上 AI 的重要变化
模型发布、价格变化、算力进展，附原始来源。免费，确认后开始发送，随时一键退订。 看一份往期日报 · 2026-11-05