Axiom 发布 Stacks Project 的 Lean 形式化库
热点事件持续更新
Axiom 发布 Stacks Project 的 Lean 形式化库
2 篇报道2 个报道来源2 小时前更新
先了解这件事
AI 综述
Axiom Math 宣布已正式验证 Stacks Project，把这部约 7500 页、奠定现代代数几何基础的开源参考书翻译成约 1600 万行经 Lean 逐行检查的代码，并作为开源库发布。公司称这填补了代数几何在形式化数学中的空白，验证结果可作为智能体后续构建软件与科学工作的可复用基础。 Axiom 表示，形式化内容、反例与修正保留在其自有仓库中，供数学家自行审阅取用。Stacks Project 维护者 de Jong 在 2026 年 10 月 21 日的公告中要求，暂不要向上游 Stacks Project 仓库直接提交 AI 生成的评论和拉取请求。
AI 根据报道生成 · 1 小时前更新
最新进展11月6日 00:16
Axiom 将约 7500 页的 Stacks Project 完整形式化为 Lean 库报道时间线
沿着报道，了解事件的不同侧面。
11月6日
- Hacker News精选Axiom 将约 7500 页的 Stacks Project 完整形式化为 Lean 库
Axiom 发布 Stacks Project 的 Lean 形式化版本，把这部约 7500 页的代数几何基础参考书变成单一机器校验库，代码约 1600 万行。
- TechCrunch · AIAxiom Math 完成 Stacks Project 形式化验证，将 7654 页数学转为 1600 万行 Lean 代码
估值 16 亿美元的 Axiom Math 宣布已正式验证 Stacks Project，其 AI 智能体团队把这一约 7654 页的数学库翻译成约 1600 万行经 Lean 逐行检查的代码。公司称这填补了代数几何在形式化数学中的空白，验证结果可作为智能体后续构建软件与科学工作的可复用基础。CEO Carina Hong 表示智能体在并行工作中自行分配任务，并已逐渐形成对数学的品味判断。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。