中国科学家人机协同破解三维Ghys猜想 获形式化验证

困扰数学界30余年的世界级数学难题——三维Ghys猜想已被成功破解。这一成果由大湾区大学许地生教授团队借助中国科学多模态大模型，通过人机协同完成证明；北京大学董彬教授、刘若川院士团队则利用自主开发的SHEAF框架，对证明完成了严格的形式化验证，确认其正确性。这标志着中国科学家首次依托本土大模型攻克了此类世界级数学难题。

Ghys猜想由法国数学家艾蒂安·吉斯于1995年提出，核心是探究紧致复流形上的全纯Anosov系统是否双全纯共轭于复 infra-幂零流形上的全纯仿射自同构。作为复动力系统领域最重要的长期公开问题之一，它兼具理论深度与学科标志性价值，是检验数学推理能力的关键试金石。若猜想成立，混乱的动力学轨迹问题可被规整为简洁的代数模型，为理解混沌系统提供核心框架。

长期深耕该领域的许地生教授，早年曾与菲尔兹奖得主阿图尔·阿维拉合作研究三维情形的Ghys猜想，但未形成有效证明思路；此后他带领学生张洁松博士，在三维情形下取得了部分弱相关结果，相关成果发表于数学顶级期刊《欧洲数学会杂志》。

2026年3月，许地生团队与AI科研团队组建联合小组，搭建了面向数学研究的Harness系统，开启了人机协同攻关。大模型凭借长链条推演优势，拆解复杂命题、并行尝试多种思路，完成了7批接续推演，问题图从15个节点扩展到389个，产出上千页严密推导，还生成数十种全新论证思路；数学家则负责把控方向，校准模型探索路径，引导其深耕关键突破口。这种紧密互动的模式，最终助力团队破解了难题，得到国际前沿学者的高度评价。值得注意的是，此前有动力系统专家尝试其他模型未获成果，印证了本土大模型在前沿数学探索中的独特价值。

AI产出的成果需经严格验证方可成立，北大团队完成了全部四个主定理的形式化验证，证明通过了交互式定理证明系统Lean的检验。整个过程仅用约5天，峰值并发达100个智能体，产出约55万行Lean代码，验证速度与并行规模均表现出色。形式化验证的难点在于需将自然语言证明转化为计算机可检查的完整逻辑，尤其动力系统领域原有形式化基础设施不足，此次工作补充了大量相关内容。北大团队用自主开发的SHEAF框架，将命题、定义及依赖组织为有向无环图，分解大规模任务为可检查步骤，确保各部分逻辑衔接。

这一研究不仅是难题的破解，更验证了一种新的科研范式：将专家直觉系统性接入机器求解回路，形成「系统探索—专家判断—成果积累—反馈修正」的闭环。不同于传统数学研究依赖个体天才的漫长摸索，这种人机协同模式可复制推广到更多搜索空间巨大、专家稀缺的基础研究领域，助力更多原始创新突破。