新快报讯 近日,困扰数学界30余年的世界级难题——三维Ghys猜想迎来了破解。大湾区大学理学院教授许地生团队依托上海人工智能实验室(上海AI实验室)书生科学多模态大模型S2,基于“通专融合”技术路径,通过人机协同完成了三维Ghys猜想证明。
北京大学董彬教授、刘若川院士团队利用其开发的SHEAF框架对本次证明完成形式化验证,验证了这一工作的正确性。这标志着中国科学家首次用中国大模型攻克世界级数学难题。
锚定世界级数学难题
科研团队开启 AI 协同研究
“Ghys猜想”由法国数学家艾蒂安·吉斯(?tienne Ghys)于1995年提出,猜测每一个紧致复流形上的全纯Anosov系统,都双全纯共轭于某个复infra—幂零流形上的全纯仿射自同构。该问题兼具理论难度与学科标志性价值,被动力系统领域数学专家公认为该领域重要的长期公开问题之一,是检验数学推理能力的一块试金石。
突破的起点,始于书生大模型在2025年全国中学生数学奥林匹克(Chinese Mathematical Olympiad,CMO)决赛中的亮眼表现。
作为大湾区大学理学院教授,许地生长期专注于动力系统、谱理论、分形几何、数学教育与AI for Math等领域的研究,在数学四大期刊等国际顶尖期刊发表了多篇论文。
许地生教授
许地生关注到书生大模型在数学方面展现出的潜力,而拿下CMO金牌后的上海AI实验室,也在探索将模型能力从竞赛级转向难度更高的研究级数学,以硬核数学难题倒逼模型能力迭代。双方目标不谋而合。
2026年初,双方正式启动模型训练合作研究。许地生教授成为上海AI实验室访问学者,双方的科研协作由此走向更深、更紧密的阶段。
人机推理攻克猜想
北大团队完成形式化核验
联合团队同步搭建面向数学研究场景的Harness系统。许地生教授结合数学科研经验,精准指出模型与系统的能力短板;依托真实前沿数学研究命题,排查出系统存在的不足,驱动系统完成多轮迭代打磨。迭代成型的书生—S2及配套系统,具备大规模递归推理能力,同时拥有高灵活性的人机交互能力,在复杂数学命题的处理能力上实现质的跃升。其中,针对三维Ghys猜想的首轮推理,书生—S2就产出了400页的推导报告。
从书生—S2提供的详尽报告中,联合团队敏锐抓住了其中的关键突破口,持续给模型反馈、校准探索方向,引导模型向着有价值的思路持续深耕,开展多轮深度人机交互,完整解决了该猜想。
攻关过程中,书生—S2先后完成7批接续推演,问题图从15个节点扩展到389个,输出总量达千页的严密推导,同时生成数十种全新论证思路,成功助力团队破解这一世界级数学难题,得到该方向国际前沿学者“思考深度远超预期”的评价。
AI助力产出的成果是否经得起验证?北京大学董彬教授、刘若川院士团队完成了本次论文全部四个主定理的形式化验证,证明已通过Lean检验。Lean作为交互式定理证明系统,能对形式化证明进行严格逻辑检查。北大团队骨干成员姜杰东、吴彬介绍,整个过程仅约5天,峰值并发达100个智能体,产出约55万行Lean代码,展现出极大的并行规模与极快的验证速度。专家确认形式化陈述与论文主定理语义一致,Lean验证据此确保其严格正确性。
接下来,依托本次研究跑通的完整能力闭环,团队将进一步封装为书生·端砚科学发现平台可复用的数学验证模块,供后续科学问题研究直接调用。
采写:新快报记者 杨英杰

暂无评论