这几天有条消息传得很广：三维 Ghys 猜想的证明做出来了，靠的是国产大模型。
事实部分先说清楚。据上海人工智能实验室和多家媒体报道：大湾区大学理学院教授许地生团队，依托上海人工智能实验室的书生科学多模态大模型 S2（书生-S2），基于「通专融合」技术路径，通过人机协同完成了三维 Ghys 猜想的证明；北京大学董彬教授、刘若川院士团队用自研的 SHEAF 框架对证明做了形式化验证。论文已上传预印本平台 arXiv，形式化代码在 GitHub 开源。
这条消息里最有信息量的地方在那句「形式化验证」，不在「攻破了」三个字。很多人把它读成「已经被机器证明是对的」，这一步读快了。
一、这是人机协同，不是 AI 独立完成官方口径写得很明确：「通过人机协同完成」。分工在报道里也有：AI 承担的是「大规模、长链条复杂数学推演」，具体的量级列得很细：首轮推理就产出 400 页推导报告，攻关过程中完成 7 批接续推演，问题图从 15 个节点扩展到 389 个，输出总量达千页，并生成数十种全新论证思路。
人做的是机器做不了的部分：判断一条思路值不值得走，以及给出下一步的直觉。报道的原话是「将专家直觉系统性接入机器求解回路」，形成「系统探索、专家判断、成果积累、反馈修正」的循环。
把这两半分清楚很重要。它说明的是「AI 能承担以前要靠人扛的那部分体力活」，也就是大规模、长链条、可拆解的推演。选题、判断哪条路有希望、判断这个结果值不值得发表，仍然在人手里。
这里还要补一句团队本身的分量。许地生长期研究动力系统、谱理论、分形几何，在 Acta Mathematica、Inventiones 等期刊发表过多篇论文，此前已在三维情形下取得部分成果，刊发于《欧洲数学会杂志》；张洁松博士从攻读博士至今一直关注 Ghys 猜想，博士导师是许地生、甘少波。这不是一个外行拿着一道难题去问模型，而是一支本来就在这个方向做了多年、离答案最近的团队，用模型把自己搜索的速度提了上去。
顺带说清「通专融合」这四个字的意思：它指的是通用大模型的能力与专业工具、专业知识结合起来使用，而不是拿一个通用模型直接去解数学题。联合团队为此专门搭了一套面向数学研究场景的 Harness 系统，用真实的前沿数学命题去排查系统的短板，再一轮轮改。
二、「验证通过」这句话，核的是哪一层央视的表述是：北大团队「通过大规模智能体并行运算，完成全部核心定理的形式化机器验证，产出数十万行验证代码，严格核验整套证明逻辑完整、无漏洞、完全成立」。
这句话描述的是逻辑层的检查：从给定的定义和前提出发，每一步推导是否合法，结论是否真的从前面推出来。这确实是一道很强的关，强到人力几乎不可能逐行核完。
但它核对的对象，是被形式化之后的那个命题，也就是先把猜想翻译成机器能读的语言，再在那个版本上做验证。「翻译得对不对、是不是忠实于原猜想」，这一步不在机器的核验范围里，仍然要人来负责。换成任何一项形式化验证的工作，这个结构都一样。
再往后一层：形式化验证通过，也不等于同行评议通过。论文目前在 arXiv 预印本阶段，形式化代码在 GitHub 开源（仓库名 frenzymath/HolomorphicAnosov），这两个动作都是公开可查的，也都是好事；但它们和「已经在期刊上正式发表」是两回事。
所以看这类消息，可以按顺序问下来：谁做的验证、验证的对象是什么、成果走到哪一步了。
三、报道里容易被略过的部分第一处：被攻克的是三维情形。 央视报道里写得很清楚：「其对应的实（数）版本至今仍是全球未解难题」。也就是说，同一个猜想的另一个版本还在那里。
第二处：有另一个模型试过这道题，没做出来。 科学网的报道里有一句：「在论文上传预印本网站 arXiv 之前，北京大学北京国际数学研究中心教授谢俊逸（2026 年国际数学家大会 45 分钟报告人）也曾用 GPT-6 尝试挑战这道题，遗憾未能找到证明方案。」这条信息几乎没有被后续报道展开，但它恰恰说明这件事并不等于「大模型都会做数学」。同一道题、不同的模型和不同的系统，结果不同。
第三处：这个模型的能力，是从一个可量化的靶子练上来的。 2025 年全国中学生数学奥林匹克（CMO）决赛首次设立 AI 测试，邀请三家国产大模型与人类选手同场答题、统一阅卷。书生-S1 拿到 102 分，在参评大模型中排第一，金牌线是 78 分。之后上海人工智能实验室做的事，是把能力「从竞赛级转向难度更高的研究级」，2026 年初与许地生启动合作，并搭建了面向数学研究场景的 Harness 系统。
这条路径值得单独记住：先有一个能反复量化的评测点，再拿它去逼真实的研究难题。 不是等到某天模型突然会做研究了。
四、这套方法能不能搬到你的方向报道给的推广条件很具体：「搜索空间巨大而专家稀缺」的基础研究领域。
但还有一条更硬的隐性条件：你的结论得能被机器逐行校验。数学能走这条路，是因为证明本身就是一个可以形式化的对象；换成实验科学，结论要落在物理世界的一次观测或一次重复实验上，形式化验证接不上这个环节。
所以判断自己领域适不适用，可以先看这个方向的核心结论能不能写成机器可校验的形式，再看这个问题是否大到单个人穷尽不过来的规模。前一条不成立时，这套人机协同能给的，会是更快的文献综述和假设生成。
五、落到你身上看到「已形式化验证」的说法，先问验证的是哪个层面的命题。这个区分以后会越来越常用：机器能核的是推导链条，人核的是命题的翻译是否忠实。
开源的形式化代码，是可以自己动手核的。GitHub 上那份代码是公开的，编译、跑一遍检查，是读者能独立做的验证动作，不需要看任何二手转述。
往后看，可以验证的是：一是这份工作是否通过同行评议、在期刊正式发表；二是如果「通专融合」这条路径真具备推广性，那么应该能在别的数学难题上看到同类的、可验证的重现，而不是只出现这一次。
本文依据上海人工智能实验室发布信息及央视、科技日报、中国科学报等公开报道整理，数学表述与过程数据均引自上述公开口径；相关结论以论文正式发表后的同行评议结果为准。
信息来源
上海人工智能实验室《中国科学家首次用中国大模型攻克世界级数学难题》央视新闻《中国科研团队依托国产大模型 攻克三维Ghys猜想世界级数学难题》科技日报《中国科学家首次用中国大模型攻克世界级数学难题》，2026 年 10 月 15 日中国科学报/科学网《国内学者使用国产大模型攻克世界级数学难题》，2026 年 10 月 15 日相关论文预印本：arXiv 2609.37695；形式化代码：github.com/frenzymath/HolomorphicAnosov