近日，中国科学院数学与系统科学研究院何伟鲲研究员带领数学机械化实验室MMAT团队，与开源 AI4Math 组织 Project Numina 及其他高校合作，完成了三维挂谷猜想这一大规模 Lean 4 形式化工作。

    本项目以 Larry Guth、王虹和 Joshua Zahl 于 2026 年给出的简化证明为主要参考，在将三维粘性挂谷情形中的关键估计作为外部输入的前提下，形式化了从该估计出发，经过指数迭代、管族体积估计，最终得到三维挂谷集合具有完整 Hausdorff 维数的整条推导链。

    本形式化项目共包含约 64.7 万行 Lean 代码、1109 个源文件和 12850 条定理及引理声明，主要依托 Project Numina 内部开发的人机交互平台 Fuse 完成。项目由数学所何伟鲲研究员统筹指导，数学机械化重点实验室王家祺、黄逸鹤、李云斐负责数学框架梳理，路线规划与定义校验，曹一川，邱瑞晨，刘俊杞组织和调度智能体开展大规模形式化工作。

   完整代码已通过构建与最终公理依赖检查。下面这行简洁的 Lean 代码，是整个项目最终抵达的形式化结论。

   > `theorem KakeyaDimensionThree : ∀ (S : Set (EuclideanSpace ℝ (Fin 3))), IsBesicovitch S → dimH S = 3`

    ## 什么是挂谷猜想？

   挂谷集合，也称 Besicovitch 集，是指在每一个方向上都包含一条单位线段的紧集。令人惊讶的是，这样的集合可以具有零体积：它在空间中“几乎不占地方”，却又能容纳朝向所有方向的线段。

    挂谷猜想断言，这类集合虽然体积可以为零，但其 Hausdorff 维数和 Minkowski 维数必须是完整的。在三维空间中，这意味着它的维数必须等于 3。

    这一问题是几何测度论中的核心难题，也与调和分析中的 Fourier 限制等基本问题密切相关。2025 年，王虹和 Joshua Zahl 宣布证明三维挂谷集合猜想；2026 年，Larry Guth、王虹和 Joshua Zahl 又给出了一套更精炼的证明。本次形式化工作主要沿用后者的证明路线。

    ## 与“三维粘性挂谷”形式化工作的关系

    此前，南开大学郭少明教授带领团队与字节跳动 Seed 合作，完成了三维粘性挂谷猜想的形式化验证。粘性情形描述了在多个尺度上具有受控组织结构的管族，是通向一般三维挂谷猜想的关键环节。

    为使两部分形式化工作能够顺利衔接，字节跳动 Seed 团队在三维粘性挂谷猜想的形式化中预留了接口。在此基础上，本项目完成了从三维粘性挂谷猜想到一般三维挂谷猜想的形式化推导。双方由此共同打通了完整证明链。至此，三维挂谷猜想的完整证明已在 Lean 4 中得到机器核验。

    ## 让前沿数学证明变得可检查、可复用、可扩展

    传统数学证明主要依靠同行逐页阅读和人工核对。形式化验证把证明写成机器可检查的对象，使计算机能够逐项核验证明的正确性。这并不能取代数学家的判断，却能为复杂证明提供一种可追踪的验证方式。从论文中的几何直觉，到 1109 个相互依赖的 Lean 文件，本项目展示了人类数学家与 AI 智能体协作处理研究级数学证明的可能性。

    本项目感谢王虹和 Joshua Zahl 在数学上的帮助与指导，并感谢马骁老师补充部分数学论证的细节。相关数学证明归功于 Larry Guth、王虹和 Joshua Zahl 及其所依托的挂谷问题研究工作；本项目的所有代码开发均由 Project Numina 李嘉领导的 Kakeya 项目支持。

---

    **相关链接**

    - Hong Wang、Joshua Zahl，*Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions*：https://arxiv.org/abs/2502.17655

    - Larry Guth、Hong Wang、Joshua Zahl，*A streamlined proof of the Kakeya set conjecture in R³*：https://arxiv.org/abs/2601.14411

    - 本项目代码仓库：https://github.com/project-numina/kakeya-3d