数学研究迎来了一位不同寻常的新“搭档”。上海人工智能实验室近日宣布，大湾区大学许地生团队依托“书生”科学多模态大模型S2，以人机协同的方式，成功证明了困扰数学界三十余年的三维Ghys猜想。随后，北京大学董彬教授与刘若川院士团队运用自研的SHEAF架构，对这一证明完成了形式化验证。据悉，这是大陆科学家首次凭借自主研发的AI大模型破解世界级数学难题。

要理解这次突破的分量，需要先回到猜想本身。Ghys猜想由法国著名数学家Étienne Ghys提出，是微分几何中叶状结构（叶层理论）领域长期悬而未决的核心问题之一，涉及三维空间中特定几何结构的存在性与分类。自猜想提出以来，三十多年间世界各国数学家围绕它展开了大量探索，尝试过多种证明路径，却始终未能给出完整而严谨的证明，其难度在学界有口皆碑。数学猜想的攻克往往需要深厚的理论积累，再加上关键时刻的灵感突破，而这一次，人工智能第一次以“合作者”的身份站上了证明一线。

据上海人工智能实验室介绍，大湾区大学许地生团队在本次攻关中采用了人机协同的研究模式。团队依托的“书生”科学多模态大模型S2，是上海人工智能实验室面向科学研究打造的多模态大模型，在数学推理与跨模态理解方面具备较强能力。在攻关过程中，AI大模型承担了海量文献梳理、证明思路探索、复杂情形验算等工作，帮助研究团队在庞大的可能性空间中快速定位有希望的证明路径；人类数学家则负责把握整体证明方向、提炼关键思想，并完成严格的逻辑论证。双方优势互补、反复迭代，最终完成了三维Ghys猜想的完整证明。这种分工并非简单的“机器算、人工看”，而是深度交织的协作：模型提出的方向需要数学家的判断来筛选，数学家的直觉也需要模型的算力来验证和拓展。

证明提出之后，如何确证其万无一失，成为下一个关键环节。为此，北京大学董彬教授与刘若川院士团队随后介入，利用自主研发的SHEAF架构对证明进行了形式化验证。所谓形式化验证，是指将数学证明转化为计算机可以逐项检查的严格形式，从而系统性地排查人工证明中可能存在的逻辑疏漏。随着现代数学证明日益复杂冗长，仅凭人工审读已难以覆盖全部细节，形式化验证正成为国际数学界确认重大成果可靠性的重要手段。此次SHEAF架构成功完成对三维Ghys猜想证明的形式化验证，不仅为这一成果加上了“双保险”，也展现了国产形式化验证工具的技术实力——从提出证明到验证证明，关键环节均由自主技术栈支撑完成。

这次突破的意义，还在于它所验证的一条新路径。数学定理证明对逻辑严密性要求极高、容错空间极小，长期以来被视为检验人工智能推理能力的“试金石”。此次大陆科学家首次用自研AI大模型破解世界级数学难题，说明国产大模型在复杂推理与科学发现方面的能力已经达到新的高度。同时，“AI辅助探索、人类主导论证、形式化验证确认”的完整链条，也为人机协同开展基础科学研究提供了一个可借鉴的范式：AI不再只是处理数据的工具，而是能够参与提出猜想、探索证明的科研伙伴。这条路径若能持续走通，未来或将有更多基础学科的难题迎来新的解法。

来源：工商时报