困扰数学界30余年的三维Ghys猜想被中国团队破解。上海人工智能实验室联合大湾区大学，用国产大模型书生-S2完成了证明，北大团队用SHEAF框架形式化验证通过。 这是中国科学家首次用中国大模型攻克世界级数学难题，相关论文已在arXiv发布，形式化代码在GitHub开源。
事件
Ghys猜想由法国数学家艾蒂安·吉斯于1995年提出，核心问题是：一个混沌动力系统的运动方式，能不能决定这个空间本身的几何形状。如果能证明，复杂的动力学轨迹问题就可以转化为简洁的代数模型。
这个问题之所以难，是因为它的实数版本至今仍是未解难题。2026年国际数学家大会45分钟报告人、北大谢俊逸教授评价：复数情形比实数情形更具刚性，研究难度极高。
那AI到底做了什么？
攻关过程中，书生-S2完成了7批接续推演，问题节点从15个扩展到389个，输出总量达上千页推导，还生成了数十种全新论证思路。许地生和团队则负责把握研究方向、判断思路价值、校准探索方向。
最终证明由北大董彬教授、刘若川院士团队验证。他们用自主研发的SHEAF框架，仅用约5天时间，峰值100个智能体并行运算，产出约55万行Lean代码，完成了全部四个主定理的形式化检验。
这里有个值得注意的细节： 在论文上传arXiv之前，北大谢俊逸教授曾用GPT-6尝试挑战这道题，没有找到证明方案。国产模型和海外顶级模型在同一问题上的表现差异，是偶然还是必然？
原因
这次突破的起点，其实是一场考试。
2025年，中国数学会首次在CMO设立AI测试，邀请三家国产大模型与人类选手同场答题。书生-S1取得102分，远超78分的金牌线，在参评大模型中排名第一。
这个成绩让许地生注意到书生大模型的数学潜力。2026年初，他受聘为上海AI实验室访问学者，双方启动联合研究，同步搭建面向数学研究场景的Harness系统。许地生结合自己的研究经验，精准指出模型与系统的能力短板，驱动完成了多轮迭代打磨。
升级后的书生-S2具备了大规模递归推理能力，针对Ghys猜想的首轮推理就产出了400页推导报告。
这说明一件事：竞赛级数学能力可以转化为研究级数学能力。 关键不在于模型本身有多强，而在于有没有懂行的人持续给出反馈、校准方向。
影响
这次突破最值得关注的不是数学本身，而是验证了一套可以复制的科研流程。
上海AI实验室将其总结为“系统探索—专家判断—成果积累—反馈修正”的闭环。通俗地说：AI负责大规模搜索和推演，人类专家负责判断哪些方向有价值、哪些思路值得深入。双方通过多轮对话迭代推进，而不是AI一次性给出答案。
这套流程正在被产品化。 上海AI实验室已经将相关能力封装为书生·端砚科学发现平台的数学验证模块，供后续研究直接调用。端砚平台覆盖从“假设提出”到“实验验证”的完整流程，已在生命科学、材料、地球气象等六大领域落地。
换句话说，这次证明不只是一个数学成果，更是一个可复用的“科研工作流模板”。
但这里有一个需要冷静看待的地方。 三维Ghys猜想的证明目前只是在arXiv上发布，尚未经过数学期刊的同行评审。形式化验证确认的是证明的逻辑正确性，但论文的学术价值还需要数学界进一步评估。
趋势
如果这套模式能跑通，影响会超出数学领域。
上海AI实验室的计划是：以Ghys猜想的突破为起点，将沉淀的推理能力扩展应用到数学结构同源的其他学科，取得新突破后再封装回平台复用，形成“突破—封装—复用—再突破”的自进化飞轮。
这个方向正在成为行业共识。 10月14日，浙江大学数学高等研究院与之江实验室联合发起“未来数学计划”，重点方向包括研发数学基础模型、开展形式化验证研究、推动数学推理成为科学基础模型的底层能力。中科院数学与系统科学研究院也在7月发布了数学机械化智能体MMAT，覆盖数学研究全流程。
海外同样在加速。Anthropic的Claude模型用11天将费马大定理证明转化为形式化证明，谷歌DeepMind发布了AlphaProof Nexus框架，解决9个未解厄多斯问题，OpenAI一次性公开了722篇AI生成的数学手稿。
一个值得关注的反常识判断是： 当AI能批量生成数学证明时，真正的瓶颈可能从“证明能力”转向“验证能力”。55万行Lean代码的验证工作，目前仍然高度依赖专业团队。谁能把验证环节的成本降下来，谁就能在这条赛道上占据先机。
陶哲轩提出的“数学2.0”概念正在被行业接受。数学家的角色从“做题的人”变成“提问题的人和判断方向的人”。这次Ghys猜想的证明过程，恰好就是这个新角色的一个样本。
你觉得这套人机协同模式，最先会在哪个学科产生下一个世界级突破？ 是数学结构同源的物理，还是数据密集的生命科学？你所在的领域，有没有类似的“搜索空间巨大而专家稀缺”的问题？
