AxiomMath 发布 1600 万行 Stacks Project 形式化，第三方抽验支持大体成立
kevrussell · x · 2026-11-06
AxiomMath 宣布发布对整个 Stacks Project（现代数学关键基础设施）的 Lean 形式化，共 1600 万行，宣称代码质量经过优化且高度互联的结构得以保留，称其为「数学城市」，作为大规模 vibecoding 的反例。
第三方 honesty.tools 随后拉取该 repo 做了一天独立核查：
- 静态扫描通过：Core 与 Frontier 部分（去注释后）中 sorry、admit、nativedecide、user axioms 均为 0，也没有 #print axioms 或 lake 构建作弊的痕迹。
- 结构：StacksCore 仅 37,588 行 / 445 文件（人工评审），约占 0.2%；其余约 1800 万行 / 62,527 文件为 AI 生成、待评审的 StacksFrontier。
- 20 条陈述抽检（N=20，非比率）：16 条吻合、1 条更强、1 条更弱、1 条相反（counterexample）、1 条不明确。
- 他们明确不背书「three-standard-axioms」相关声明，仍有很多内容未检查。
所属事件:Axiom Math 将整个 Stacks Project 形式化为 1580 万行 Lean 代码(10 条相关)→
「编程与Agent」频道最新
- Weaver 框架：增量推理从历史对话中检索并追踪用户偏好适用范围 — _reachsumit · 2026-11-06
- VoidZero 发布 tsrs：Rust 版 TypeScript 快 8 倍省 70% 内存，公司并入 Cloudflare — cnakazawa · 2026-11-06
- 68 个 Codex 插件里 35 个两周没用：闲置插件正在白吃你的上下文窗口 — nickbaumann_ · 2026-11-06
- 论文提出多开发者智能体系统MDA:沿开发者维度扩展AI编程 — karthik_r_n · 2026-11-06
- Codex 挂机跑 33 小时改 115 个文件,「GPT-6 Sol Ultra」梗图流传 — dscape · 2026-11-06
- Stagehand 4.4 发布：浏览器可断开重连，接入 LangChain deep agents — LangChain · 2026-11-06