上海人工智能实验室访问学者、大湾区大学教授许地生团队，依托书生科学多模态大模型S2（书生-S2），以人机协同方式完成了三维Ghys猜想的证明。北京大学董彬教授、刘若川院士团队随后利用自主开发的SHEAF框架对证明进行形式化验证，全部四个主定理通过Lean检验。相关论文已发布在预印本平台arXiv，形式化代码在GitHub公开。

Ghys猜想由法国数学家艾蒂安·吉斯于1995年提出，核心问题是：混沌的动力系统行为能否决定几何上的分类。通俗理解，若一个封闭、无边界且局部遵循复数运算规则的“世界”中存在某种既混沌又完全规则的运动，那么这个世界的形状就只能是由简单规则反复拼接的高度规整结构，例如复环面，其运动本质上只是平移、旋转或缩放。该猜想被动力系统领域专家公认为最重要的长期公开问题之一，也是检验数学推理能力的试金石。

许地生长期研究这一猜想，曾与其导师、菲尔兹奖得主阿图尔·阿维拉合作探索三维情形但未形成有效证明思路，此后与学生张洁松合作取得部分弱相关结果，刊发于《欧洲数学会杂志》。2026年3月，许地生成为上海AI实验室访问学者，双方组建联合团队并搭建面向数学研究的Harness系统。8月，内部迭代成型的书生-S2具备大规模递归推理与灵活人机交互能力，针对三维Ghys猜想的首轮推理即产出400页推导报告。

技术层面，团队坚持“通专融合”路线，在大规模科学知识预训练基础上构造研究级后训练数据，并突破异步长程推理强化学习训练方法，解决误差指数级累积、长期状态维护与自我纠错等难题，还将Harness带来的能力提升反向蒸馏回模型。在IMO-Proof、AdvancedMathBench等基准上，书生-S2整体领先现有开源模型，部分指标超越Gemini 3.1 Pro等闭源模型。

攻关过程中，书生-S2先后完成7批接续推演，问题图从15个节点扩展到389个，输出总量达上千页严密推导，并生成数十种全新论证思路。研究人员负责把握方向、判断思路价值并给出直觉建议，模型承担海量繁琐推导，双方通过多轮对话迭代推进。值得注意的是，动力系统专家谢俊逸教授此前曾用GPT-6尝试该题未找到证明方案，这从侧面印证了书生-S2在本次探索中的独特价值。

验证环节，北大团队完成论文全部四个主定理的形式化验证。骨干成员姜杰东、吴彬介绍，整个过程仅约5天，峰值并发达100个智能体，产出约55万行Lean代码。形式化难度不仅来自数学本身——自然语言证明常依赖读者补全条件，形式化须落实为计算机可检查的完整证明——还因动力系统领域原有形式化基础设施不足，此次补充了大量基础设施。团队使用SHEAF框架，将命题、定义及依赖关系组织成从目标定理逐层延伸到基础定理库的有向无环图，把大规模形式化任务分解为可检查的步骤。

北大数学团队早在2021年便布局AI for Math方向，搭建了覆盖高难度评测集FATE、数学知识检索Matlas/LeanSearch、自动推理与形式化验证Rethlas/Archon/Danus/Iteris的完整技术链条，其AI系统曾攻克安德森猜想，近期还独立完成庞加莱猜想的形式化验证。

本项研究的意义还在于验证了一种新科研范式：将专家直觉系统性接入机器求解回路，形成“系统探索—专家判断—成果积累—反馈修正”的闭环。这一范式可复制到更多“搜索空间巨大而专家稀缺”的基础研究领域。接下来，团队将把跑通的能力闭环封装为书生·端砚科学发现平台可复用的数学验证模块，并以三维Ghys猜想为起点，将推理能力扩展至数学结构同源的其他学科，形成“突破—封装—复用—再突破”的自进化飞轮。