中国数学家携手大模型攻克三维Ghys猜想，北大团队完成形式化验证

困扰数学界三十余年的世界级难题——三维 Ghys 猜想正式迎来破解。大湾区大学教授许地生团队借助中国科学多模态大模型，通过人机协同方式完成了该猜想的证明工作。北京大学董彬教授、刘若川院士团队利用其开发的 SHEAF 框架对此次证明结果进行了形式化验证，确认了工作的正确性，这标志着中国科学家首次利用国产大模型攻克世界级数学难题。「Ghys 猜想」由法国数学家艾蒂安·吉斯（Étienne Ghys）于 1995 年提出，其核心命题猜测每一个紧致复流形上的全纯 Anosov 系统，都双全纯共轭于某个复 infra-幂零流形上的全纯仿射自同构。该问题兼具极高的理论难度与学科标志性价值，被动力系统领域专家公认为该领域最重要的长期公开问题之一，是检验数学推理能力的重要试金石。为解决这一关于混沌系统「底层代码」的难题，许地生教授于 2026 年 3 月与国内某 AI 实验室组建联合团队，并搭建了面向数学研究场景的 Harness 系统。针对首轮推理，模型输出了长达 400 页的推导报告。科研团队坚持「通专融合」技术路线，在大规模科学知识预训练基础上构造研究级后训练数据，并突破异步长程推理强化学习训练方法，有效破解了误差累积与自我纠错等根本性难题。在人机协同攻关过程中，大模型发挥长链条大规模推演优势，拆解复杂命题并猜想不同思路；研究人员则负责把握方向，判断路径价值并提供直觉建议。通过多轮对话与反馈迭代，系统在首轮探索基础上完成了 7 批接续推演，问题图节点从 15 个扩展至 389 个，输出总量达上千页严密推导，成功助力团队破解该难题。为确保成果经得起检验，北京大学董彬教授、刘若川院士团队对论文全部四个主定理完成了形式化验证，证明已通过 Lean 交互式定理证明系统检验。整个过程历时约 5 天，峰值并发智能体数量达 100 个，产出约 55 万行 Lean 代码。北大团队骨干成员姜杰东、吴彬指出，该工作利用自主开发的 SHEAF 框架，将大规模形式化任务分解为相互衔接且可检查的步骤，确保定义准确与证明链完整。相关论文已在预印本平台 arXiv 发布（链接：https://arxiv.org/pdf/2609.37695），其形式化代码也在 Github 平台公开（链接：https://github.com/frenzymath/HolomorphicAnosov）。这一成果不仅印证了国内大模型在前沿数学探索中的独特价值，也标志着中国科技力量正式站上世界级数学难题攻关的赛场。相关研究成果由许地生教授及其学生张洁松博士主导，其中许地生曾与菲尔兹奖得主阿图尔·阿维拉（Avila）教授合作研究三维情形，后于 2026 年实现关键突破。国际数学家大会将于 2026 年召开，北京大学北京国际数学研究中心谢俊逸教授对此评价称，复数情形的 Ghys 猜想是刚性现象研究中的重要问题，非常困难，而本次人机协同的成功为类似基础难题提供了新的解决思路。此次突破显示了中国科学多模态大模型在辅助科研方面的潜力，特别是在处理高难度、长链条推理任务时的表现。从单克隆抗体到纳维 - 斯托克斯方程，再到如今的三维 Ghys 猜想，人工智能正逐步介入人类智力活动的深水区，为古老而基础的科学问题提供新的解题工具。