科技日报记者 杨雪
据南开大学公众号消息，南开大学讲席教授郭少明团队与字节跳动Seed合作，近日完成三维粘性挂谷猜想的形式化验证，代码已在开源平台GitHub发布。
挂谷猜想是调和分析与几何测度论领域的百年难题。2025年，数学家王虹与约书亚·扎尔证明三维挂谷猜想；2026年7月，王虹凭借包括这项工作在内的成果获菲尔兹奖，扎尔现为南开大学陈省身数学研究所讲席教授。
三维粘性挂谷猜想是上述证明中的关键一环。形式化验证是将数学证明转化为计算机可核验的代码，通常使用Lean等定理证明器完成。
据南开大学公众号介绍，此次工作共完成约180万行Lean代码，其中约90%由字节跳动Seed团队研发的Seed-Prover生成。Seed-Prover以Seed-Evolving为模型底座，采用多智能体协作方式大规模并发形式化。数学论证梳理及部分代码由郭少明带领陈铭峰、庞逸轩、沈敏行完成。
在南开大学与字节Seed的工作基础上，中国科学院数学与系统科学研究院团队与开源人工智能数学组织Project Numina合作，进一步完成了从三维粘性挂谷猜想到一般三维挂谷猜想的形式化推导，三维挂谷猜想的完整证明由此实现形式化验证。字节跳动Seed团队在前期工作中预留接口，使两部分顺利衔接。
网友评论
