还记得去年大家还在讨论大模型做小学奥数题能不能及格吗？就在2025年的平安夜，字节跳动Seed团队甩出了一个重磅炸弹：Seed Prover 1.5。
这不是一次普通的版本更新，这更像是一个只会做选择题的学生，突然进化成了能写出严谨证明过程的数学家。简单来说，这个AI现在不仅能做题，还能用Lean语言写出可被计算机编译验证的代码，直接把从本科到博士难度的数学题“拿捏”了。
作为一名长期关注AI进化的观察者，看完他们的技术报告，我最大的感受是：AI解题的逻辑变了。
哪怕是陶哲轩看了也要愣一下的战绩
先别管技术细节，我们直接看这东西到底有多强。
团队拿它去跑了2025年的国际数学奥林匹克（IMO）真题。结果是，在前5道题里，它拿下了35分（满分42）。这个分数意味着什么？意味着它已经稳稳地拿到了金牌。而且，它不是那种“我觉得答案是X”的模糊回答，而是在16.5小时内，生成了完整、可运行、逻辑无懈可击的Lean证明代码。
再看被称为“北美最难本科数学竞赛”的Putnam竞赛。2025年的12道赛题，它搞定了11道，耗时不到9小时。而在Putnam的历史题库里，它的解决率飙到了88%，刷新了目前的世界最佳纪录。
更有意思的是，在代表硕士难度的Fate-H测试集中，它的解决率是80%；到了博士难度的Fate-X，虽然降到了33%，但也足以让很多在该领域摸爬滚打的人类研究员感到背脊发凉。
不再是“瞎猜”，而是像人一样思考
以前的大模型做数学题，很多时候像是在“背题库”或者“文字接龙”，一旦逻辑链条太长，它就开始胡言乱语。
Seed Prover 1.5 的核心突破在于，它换了一种活法。字节跳动这次搞出了一个全新的架构，叫 Agentic Prover。
你可以把它想象成一个坐在图书馆里的研究员，而不是一个只会答题的机器。
首先，它学会了用工具。 以前的模型是一口气把答案憋出来，憋错了就完了。Seed Prover 1.5 不一样，它把自己当成一个智能体（Agent）。在证明过程中，它会去查阅数学库（Mathlib），看看有没有现成的定理可以用；它甚至会写一段Python代码来验证自己的某个猜想对不对。这种“增量式”的解题方式，允许它一步步搭建证明的大厦，而不是试图一步登天。
其次，它有了“直觉”。 数学证明最难的是从自然语言的“思路”到形式化代码的“落地”。团队给它装了一个“Sketch Model（草图模型）”。这就好比人类数学家解题时，先在草稿纸上画出大概的思路框架，有了这个直觉引路，再把复杂的命题拆解成一个个小问题，最后才去写那些严谨枯燥的代码。
最后，它是被“骂”出来的。 训练这个模型用的是大规模强化学习。它的老师是铁面无私的Lean编译器。代码写对了就是对，写错了就是错，没有中间地带。在这种绝对客观的反馈下，模型在数百万次的尝试中，硬生生把解题成功率从50%练到了90%。
还是有局限，但未来已来
当然，要把它吹成“数学之神”还为时尚早。
Seed团队自己也很诚实，他们在报告里坦言，目前的Seed Prover 1.5 还是个“竞赛型选手”。它最擅长的是那些规则清晰、背景封闭的竞赛题。如果你扔给它一篇几十页的前沿数学文献，让它基于此进行长链条的复杂推理，它可能还是会懵圈。
但这并不妨碍它的里程碑意义。
它证明了机器不再仅仅是语言的模仿者，而是开始具备了严谨逻辑的探索能力。当AI开始学会像数学家一样查资料、写草稿、验证猜想，并最终给出一段可编译的证明代码时，我们距离那个能在科研领域辅助人类突破未知的AI助手，其实已经不远了。
对于数学系的学生和AI研究者来说，Seed Prover 1.5 的API后续开放，绝对是一个值得第一时间去排队体验的大事件。毕竟，谁不想看看这个拿了IMO金牌的“硅基大脑”，到底是怎么思考的呢？
如果你也对最新的AI信息感兴趣或者有疑问 都可以加入我的大家庭 第一时间分享最新AI资讯、工具、教程、文档 欢迎你的加入！！！😉😉😉
公众号：墨风如雪小站
