3D Kakeya 猜想在 Lean 中完成完整形式化，AI4Math 助力机器验证证明
AlexKontorovich · x · 2026-09-09
Jia Li 宣布 3D Kakeya 猜想的证明已在 Lean 4 中完成形式化，项目已开源在 GitHub（project-numina/kakeya-3d）：
- 形式化基于 Guth–Wang–Zahl 的证明，从 Sticky Kakeya 定理出发；结合南开大学 × 字节跳动 Seed AI4Math 团队完成的无条件 Sticky Kakeya 形式化，整个证明无 sorry、无项目专属公理，完全机器验证；
- 证明分两层：KakeyaDimensionThree 从一个显式数学输入（GWZ 定理 7.3(A) 的 StickyFrostmanHypothesis 表述）推出猜想，KakeyaDimensionThreeofpureWZ2 消去该输入，得到无条件结论；
- 3D Kakeya 猜断言 R³ 中每个方向都包含单位线段的紧集 Hausdorff 维数为 3，是近年组合几何的重大突破。
作者称这是「AI 帮助把前沿数学变成机器验证证明」的典范案例。
「研究」频道最新
- IFM 开源 K2 Horizon 全家桶:6 个尺寸、每模型 20T tokens、连 reward-hacking 审计都公开 — kimmonismus · 2026-09-09
- 开发者上线聚合站，汇集 OpenAI 纳维-斯托克斯证明各方表态 — NathanpmYoung · 2026-09-09
- Astra 自研国际象棋战术引擎文档曝光，可强制或阻止特定结果 — MikePFrank · 2026-09-09
- Anshul Kundaje：基因组学正处于技术突破的黄金期 — anshulkundaje · 2026-09-09
- 斯坦福 Kundaje:ML for Bio 领域该改革同行评议评价体系了 — anshulkundaje · 2026-09-09
- JASPAR 2026 发布大幅扩充,将与 DeepMind 合作统一 DNA motif 库 — anshulkundaje · 2026-09-09