AI 助力证明三维 Ghys 猜想，证明还过了形式化检验

一道悬了三十多年的数学难题，最近多了一份由大模型参与完成的证明——而且这份证明被另一个独立团队用机器逐行验过了。

一、发生了什么

据雷峰网报道，上海人工智能实验室访问学者、大湾区大学教授许地生团队，依托书生科学多模态大模型「书生-S2」，以人机协同方式完成了三维 Ghys 猜想的证明。这道猜想由法国数学家吉斯于 1995 年提出，被动力系统领域视为最重要的长期公开问题之一，大意是说：某类足够「混沌」的规则运动，反过来只能存在于极其规整的几何形状上。粗略地讲，混乱的运动方式决定了世界的形状没得选。

攻关方式值得细看。模型负责铺开多条支线、拆解命题、承接海量推导；数学家负责判断哪些思路值得深挖、哪些是死胡同。从今年 3 月组建联合团队到 8 月系统成型，首轮推理就产出 400 页推导报告；整个攻关完成七批接续推演，问题分解图从 15 个节点扩到 389 个，总输出上千页。

验证环节交给了北京大学团队。董彬教授、刘若川院士团队用自研框架对论文全部四个主定理做形式化，约五天完成，峰值一百个智能体并行，产出约 55 万行 Lean 代码，确认形式化陈述与论文语义一致。论文已挂预印本，形式化代码也公开了。

几点背景需要分开：这是机构发布的成果口径；有动力系统专家评价其「思考深度远超预期」；另有一位北大教授此前用别家顶尖模型挑战此题未果，此事被引用来说明本次路径的独特性，属于发布方的叙述。

二、跟你有什么关系

如果你做 AI 研发：这是一次「长程推理 + 可验证奖励」的实战样本，递归推理、误差累积、自我纠错这些工程问题的解法有参考价值。

如果你在学术界：人机协同的新范式是「系统探索—专家判断—反馈修正」的闭环，适合搜索空间巨大而专家稀缺的领域，但专家的方向感仍是不可替代的一环。

如果你是普通读者：记住验证这条线。AI 参与的数学成果，可检验性比「谁做的」更重要，Lean 这类证明助手给出了客观裁判。

三、怎么评估这类成果

1. 先看是否通过形式化验证。自然语言证明依赖读者脑补，Lean 检验过的证明才排除了逻辑漏洞。

1. 分清模型贡献与人贡献。此次是数学家抓住关键突破口、模型承担大规模推演，宣传成「AI 独立证出猜想」就是误读。

1. 等独立复用。这套流程封装成平台模块后，能否在其他学科复制突破，才是范式成立的真正检验。

四、三个别信的说法

「大模型取代了数学家。」 模型干的是海量试错和推导执行，关键直觉、方向校准都来自人。没有许地生团队三十年积累，机器无从下手。

「AI 做数学不可信。」 恰相反，形式化验证让机器参与的结果比纯人证更可查——每一步都被程序核对过。

「模型竞赛数学分数高就能攻难题。」 竞赛题有标准答案、几小时内可解；研究级问题要数月推演和方向判断，是两种能力。发布方也承认基模能力只是「基本水平」，协同才是关键。

五、一句话结论

AI 在数学里先拿到的是「苦力活」，人握着方向盘，而 Lean 负责验货。

信息来源

• 雷峰网：《书生-S2 助力三维 Ghys 猜想证明并通过形式化验证》，2026 年 10 月：原文

功能与价格以官方公告为准。本文写于 2026 年 10 月 25 日。