中国大模型立功！数学家攻克30年世界难题

困扰数学界30余年的三维Ghys猜想迎来破解。大湾区大学教授许地生团队借助中国科学多模态大模型，通过人机协同完成三维Ghys猜想证明。北京大学董彬教授、刘若川院士团队利用其开发的SHEAF框架对证明完成形式化验证，确认其正确性。这标志着中国科学家首次用中国大模型攻克世界级数学难题。相关论文已在arXiv发布，形式化代码在Github公开。

Ghys猜想由法国数学家艾蒂安·吉斯于1995年提出，猜测每一个紧致复流形上的全纯Anosov系统，都双全纯共轭于某个复infra-幂零流形上的全纯仿射自同构。该问题被动力系统领域专家公认为该领域最重要的长期公开问题之一。其核心是：混沌的动力系统行为的存在是否能决定几何上的分类。若猜想成立，混乱的动力学轨迹问题就能化归为简洁、规整的标准代数模型。2026年国际数学家大会45分钟报告人、北京大学谢俊逸教授评价，该猜想对应的实版本类似断言仍是著名完全公开难题，复数情形更加刚性，非常困难。

许地生长期深耕该猜想，曾与导师、菲尔兹奖得主阿维拉合作研究三维情形但未形成有效证明思路；此后与学生张洁松合作取得三维情形部分弱相关结果，刊发于《欧洲数学会杂志》。

2026年3月，许地生团队与国内某AI实验室组建联合团队，搭建面向数学研究场景的Harness系统。首轮推理模型产出400页推导报告。团队坚持“通专融合”路线，突破异步长程推理强化学习训练方法，破解误差指数级累积、长期状态维护、自我纠错等难题，并研发能力反向蒸馏的自进化算法。攻关中，大模型完成7批接续推演，问题图从15个节点扩展到389个，输出上千页严密推导，生成数十种全新论证思路。许地生与张洁松在首轮探索基础上抓住关键突破口，持续反馈校准方向。成果获国际前沿学者“思考深度远超预期”评价。谢俊逸曾用GPT-6尝试挑战该题，未找到证明方案。

北大董彬、刘若川团队完成论文全部四个主定理的形式化验证，通过Lean检验。骨干成员姜杰东、吴彬介绍，整个过程仅约5天，峰值并发达100个智能体，产出约55万行Lean代码。专家确认形式化陈述与论文主定理语义一致。动力系统领域原有形式化基础设施不足，此次补充了大量基础设施。团队使用自主开发的SHEAF框架，将命题、定义及依赖关系组织成有向无环图，分解大规模形式化任务。

北大数学团队是国际上最早布局AI for Math的研究团队之一，搭建覆盖高难度评测集、大规模数学知识检索、自动推理与形式化验证的完整技术链条，曾攻克安德森猜想，近期独立完成庞加莱猜想的形式化验证。本项研究验证了一种新科研范式：将专家直觉系统性接入机器求解回路，形成“系统探索—专家判断—成果积累—反馈修正”闭环，可推广至更多“搜索空间巨大而专家稀缺”的基础研究领域。