Axiom 用 Agent 把整个 Stacks Project 变成 1600 万行经机器验证的 Lean
LinusEkenstam · x · 2026-11-05
Axiom 发布了对整个 Stacks Project 的形式化成果：将代数几何界二十年积累的标准参考文献完整转化为 Lean，共约 1600 万行代码，每一行都经过计算机验证——要么成立，要么编译不通过。
更难得的是结构保留：Stacks 是一张结果相互依赖的巨大网络（作者比作卢浮宫玻璃金字塔），他们原样保留了这种高度互联的结构，只是换成了机器可检验的形式。团队像软件团队一样组织 agent：一部分负责架构、一部分负责核心定义、一部分负责单个证明。
这是对「大规模 vibecoding 只会产出垃圾代码」这一普遍印象最有力的反例。
所属事件:Axiom Math 完成整个 Stacks Project 的 Lean 形式化(7 条相关)→
「编程与Agent」频道最新
- 把 thinking 拉满再用 Claude:省下追问成本换来自主性 — curious_vii · 2026-11-05
- MCP 适合构建不适合运行:Swytchcode 提出"构建+运行时"分离方案 — curiousblack99 · 2026-11-05
- Yuchen 宣称「Codex 赢下了 Agent 之战」 — Yuchenj_UW · 2026-11-05
- 用 Opus 5.5+Blender+Three.js 做交互式家庭应急教学页 — techartist_ · 2026-11-05
- 开发者提出 0-12 级 AI 开发自主度量表，以谁干活为轴 — nimareq · 2026-11-05
- Claude 官方 Cookbook：给 Agent 搭「做梦」服务，夜间自动蒸馏记忆 — brada · 2026-11-05