Axiom 用 AI 完成整个 Stacks Project 形式化，1600 万行 Lean 代码
kimmonismus · x · 2026-11-05
Axiom 宣布完成整个 Stacks Project 的 Lean 形式化，共 1600 万行代码，这是现代代数几何的关键基础设施。这被视为「AI 大规模写代码是 slop」这一论调的有力反例。
关键点：
- 规模与结构并重：Axiom 将其比作卢浮宫玻璃金字塔——每个定义和证明都必须精确衔接，一章证明的结果可以在另一章复用，保留了原项目高度互联的结构。
- 不只是翻译：由人类协调的 AI agent 集群（swarm）构建出一个可复用、机器可验证的数学基础，后续 AI agent 可以在此基础上直接做数学研究。
- 这类大规模形式化此前被认为远超 AI 能力范围，本次发布是 AI4Math 的标志性成果。
所属事件:Axiom 用 AI 将 Stacks Project 全部形式化为 1600 万行 Lean 代码(6 条相关)→
「研究」频道最新
- 研究：Claude 多轮交流中自创符号，从螺旋 🌀 漂移到粉心 💖 — mimi10v3 · 2026-11-05
- Engram 团队：少量训练即可修复长时程模型的不可读笔记 — scott_linderman · 2026-11-05
- SkyDiscover 自动合成推理引擎,Mac 上快 2.7 倍 — CShorten30 · 2026-11-05
- NMSLIB 作者公开质疑新向量检索论文漠视其开创性贡献 — srchvrs · 2026-11-05
- NMSLIB 作者:新论文未证实「多表示降低性能」论断 — srchvrs · 2026-11-05
- Foresight-SWE 基准:编程智能体解题 60.7%,却只有 14.8% 不埋新 bug — OfirPress · 2026-11-05