Stacks Project 启动 Lean 形式化:代数几何全书证明交由内核验证
rohanpaul_ai · x · 2026-11-05
代数几何领域权威开源参考书 Stacks Project 正被形式化为 Lean 定义与证明,构建于 Mathlib 之上,由 Lean 内核对每条完成的证明进行自动检查。
- 项目中每个带四字符标签的定义、引理、命题与定理都有对应 Lean 形式化,每个标签可链接到其 Lean 代码与依赖关系。
- 站点提供交互式依赖图、树图与「城市」可视化,可按 parts/chapters/sections 浏览并查看声明之间的依赖层级。
- 绿色标签表示已被 Mathlib 收录,红色标签则被判定不适用于 Lean 形式化。
- 项目欢迎社区贡献,目标是审校、完善并尽可能将成果上游合入 Mathlib。
所属事件:Axiom 用 AI 将 Stacks Project 全部形式化为 1600 万行 Lean 代码(6 条相关)→
「研究」频道最新
- 多态界面从头设计：蛋白质组件可在多种几何间切换 — DaveJuergens · 2026-11-05
- 斯坦福实测:同样耗电下 NVIDIA B200 价值产出是 AMD MI350X 的 4 倍 — rohanpaul_ai · 2026-11-05
- ReuseGR 论文：7B 离线规划+0.5B 在线补全，解耦生成式检索降解码成本 — _reachsumit · 2026-11-05
- ZeroGR：先过滤再评分，生成式推荐解码提速最高 9.9 倍 — _reachsumit · 2026-11-05
- 字节跳动 OneTrans-GSR：用单个自回归模型统一重排与混排 — _reachsumit · 2026-11-05
- 数据受限稠密检索的 Scaling Law：BERT 系检索器符合乘性幂律 — _reachsumit · 2026-11-05