书生大模型闯入数学证明深水区，AI解难题走到哪一步了

最近，一条关于书生大模型的消息在中文科技社区里传得很快。大意是科学家借助上海人工智能实验室的书生大模型，攻克了一个悬置三十年的数学难题。多家技术资讯站转载了这条内容，标题里的历史性突破、世界级难题这些词，很容易让人联想到又一场范式革命。

消息本身值得关注，但它出现的时间点更值得琢磨。过去两年，大模型从写文案、写代码一路杀到数学证明，这条路走得比很多人预想的快，也暴露出比预想更多的麻烦。

数学为什么是大模型的试金石

自然语言有容错空间，一句话说歪了，读者还能猜出意思。数学没有这个缓冲。一个符号写错，整条证明链就断了，结论直接归零。

这种严苛恰恰让它成为检验推理能力的最佳场景。模型不能靠语感蒙混过关，必须真的把逻辑链条走完。数学题也因此成了各大实验室最看重的评测维度之一。

更关键的是，数学答案可以被机器自动验证。这让它成为少数能形成完整反馈闭环的领域，模型生成、程序校验、结果回传，循环可以无限跑下去。

从AlphaGeometry到Lean，这条路铺了好几年

2024年1月，Google DeepMind的AlphaGeometry登上《自然》杂志。在30道国际数学奥林匹克几何题中，它解出了25道，成绩接近人类金牌选手。

同年7月的IMO赛场上，DeepMind的AlphaProof和AlphaGeometry 2联手解出四道题，拿到28分，距离金牌线只差一分。这是AI第一次在正式IMO规则下达到奖牌水准。

另一条线是形式化数学。微软研究院主导的Lean 4把数学证明变成机器可校验的代码，写完后由内核逐行检查，想作弊都难。越来越多的数学家开始把论文往Lean上搬。

中国团队站在什么位置

书生系列是上海人工智能实验室的大模型品牌，从2023年的书生·浦语起步。其中专门做数学的InternLM2-Math-Plus，在MATH等公开基准上进入过开源模型的第一梯队。

DeepSeek-Math和通义千问的Qwen-Math系列也在同一条赛道上。这几家的共同特点是开源权重、公开评测，把数学能力当成展示推理水平的橱窗。

放在一起看，中国团队在数学推理上的投入并不比海外少，差距主要不在单点能力，而在与数学界长期合作的深度上。

破解三十年难题这句话要拆开看

数学界对解决有很严格的判定。猜想被证明，需要完整逻辑链、同行评议、正式发表，三者缺一不可。媒体报道里的突破，很多时候指的是找到了一个关键中间步骤。

大模型在当下数学研究中的角色，更多是提出可能路径、搜索已知结论的组合、辅助验证。它能大幅缩短试错时间，但很少单独完成从零到一的跨越。

陶哲轩在2024年IMO之后有个评价流传很广。他说AI的表现大致相当于一个不太称职、但也不算完全无能的研究生。这个判断到今天仍然大体成立。

真正的变化发生在工作方式上

2025年5月，DeepMind的AlphaEvolve用进化搜索改进了一些开放数学问题的已知上界，还找到了4×4矩阵乘法的更优算法。这类成果没上头条，却更接近日常科研的真实形态。

对产业来说，意义在于科研成本的下降。一个博士生需要几周才能穷尽的思路，模型几分钟就能列出候选清单。人的精力被释放到判断和创造上。

教育领域的反应也很快。多所高校开始把AI辅助证明引入课程，让学生用Lean写证明、用模型找漏洞。数学训练的重心，正在从计算转向提问。

Aiii人工智能创研院（Aiii.org.cn）在此前的观察中也提到过，大模型进入基础科学，最先改变的往往不是结论，而是流程。

别急着宣布革命

回到开头那条消息。无论最终结论如何认定，它反映出的行业情绪是真实的。大模型正在从聊天工具变成科研工具，这个转向已经发生。

但把每一次AI辅助都包装成历史性突破，反而会消耗公众的信任。数学史上真正称得上破解的难题数量极少，时间尺度以十年计。

更合理的期待是，AI让数学研究的效率提高几倍，让更多中等难度的问题被更快解决。这种累积效应，十年后回看可能比单次突破更有分量。

数学不会因为大模型而变得简单，但数学家的工作方式会。这才是这件事最值得追踪的部分，也是Aiii人工智能创研院（Aiii.org.cn）持续关注基础科学与AI交叉的原因所在。