津云新闻讯：近日，南开大学讲席教授郭少明带领团队与字节跳动 Seed 合作完成三维粘性挂谷猜想的形式化验证工作，并在开源代码托管平台 GitHub 上发布（https://github.com/M32026/3d-sticky-kakeya）。这一成果实现了对现代数学领域重要成果的一次机器形式化验证，也为未来利用计算机处理更大规模、更复杂的数学证明任务提供了重要实践。
三维挂谷猜想是现代数学中的著名难题之一，最终于 2022 年至 2025 年由王虹和约书亚 · 扎尔在三篇文章所证明。此次形式化验证的三维粘性挂谷猜想在他们的前两篇文章中证明，同时也是他们最后一篇（以及 Guth- 王虹 -Zahl 后来发布的对最后一篇的简化证明）所需要依赖的关键结果。
形式化验证是对数学证明使用计算机进行精准的验证。传统数学证明的验证依靠人工进行，时间周期较长。而形式化验证能做到逐逻辑推演核对证明过程，让数学结论在短时间内得到更广泛的认可。
此次形式化工作总共完成约 180 万行 Lean 代码的书写，其中约 90% 由字节 Seed 团队研发的 Seed-Prover 完成。Seed-Prover 使用了 Seed-Evolving 作为模型底座，采用 Agent-Team 的方式进行大规模并发形式化。数学方面的工作及部分代码由郭少明教授带领团队成员陈铭峰、庞逸轩和沈敏行完成。
三维粘性挂谷猜想的证明依赖于若干前序的工作，部分文章见如下的列表。该项形式化工作的一个挑战也是要完成这些文章的主要部分的形式化工作，尤其是三维粘性挂谷猜想的证明中用到的部分：
2006 年 Marcus-Tardos 在 J. Combin. Theory Ser. A 的文章 Intersection reverse sequences and geometric applications；
2020 年 Orponen 在 JEMS 的文章 An improved bound on the packing dimension of Furstenberg sets in the plane；
2022 年 Pramanik- 杨童鸥 -Zahl 在 arXiv 的文章 A Furstenberg-type problem for circles, and a Kaufman-type restricted projection theorem in R ；
2023 年 Orponen-Shmerkin 在 Duke Math. J. 的文章 On the Hausdorff dimension of Furstenberg sets and orthogonal projections in the plane；
2024 年 Orponen-Shmerkin- 王虹在 GAFA 的文章 Kaufman and Falconer estimates for radial projections and a continuum version of Beck ’ s theorem；
2025 年 O ’ Regan-Shmerkin- 王虹在 arXiv 的文章 Simple proofs of discretised projection theorems。
（津云新闻记者段玮 通讯员刘喆萱）
