周三下午三点，哈佛大学数学科学及应用中心的一间会议室里，没有咖啡香，只有叹息声。几位数学家围坐在长桌旁，每人手里都攥着同一批考卷——但出题的和答题的，都不是人类。这是全球最硬核的“AI数学高考”第一次正式放榜，而改卷老师们正经历着一种奇特的精神分裂：一边惊叹，一边想撕卷子。
这场考试有个很正经的名字——“一阶证明”。发起人是一群对AI公司宣传相当不满的顶尖数学家。过去两年，科技公司喜欢拿高等数学竞赛题给自己的大模型背书，仿佛解出几道IMO真题，就算踩进了数学家真正的领地。但工程师眼里的天花板，在数学家看来只是地板。于是他们干脆自己搭了个擂台：不出竞赛题，专挑数学科研中那种需要创造性、推理链长、参考文献跨领域的问题。
今年二月那一轮摸底考，成绩就像开盲盒。有些公司的内部定制模型遥遥领先，但公开版的表现则像是两个物种。为了杜绝“特供版”刷榜，刚过去的这一轮测试定下一条硬规矩：只测公开可用的模型。哈佛大学数学家、一阶证明团队成员劳伦·威廉姆斯说得直白：“我们强烈地觉得，如果你说在为更大的社区做公共服务，那就必须测公开模型。拿私藏版本出来给大家看成绩单，那叫耍赖。”
这一刀，直接砍掉了大部分参赛者。最后只有OpenAI和三个学术小组——瑞士苏黎世联邦理工学院、丹麦奥胡斯大学组成的联合队，以及加州大学洛杉矶分校和普林斯顿大学各自搭建的模型——走到了对战的格子间前。考试用题是从数学各分支领域广泛征集来的，涵盖了纯数学和应用数学里真正会让博士生头疼的问题。而评卷环节更是专业到有点“奢侈”：团队花钱请来了专家级的评分人，把审核AI生成的证明当成一项苦差摊派。
威廉姆斯回忆起这个过程时用了“痛苦又没人感激”来形容。一群职业数学家花了整整两天时间，在哈佛的这间屋子里进行高强度“同行评审”——正常数学论文的审稿动不动拖上大半年，而他们要在48小时内阅读一堆混着真知灼见和胡言乱语的长篇答案。有人把这次经历叫做“淘金”：你得筛掉成吨的泥沙，才能找到针尖大的一点亮光。
这筛出来的结果，就是一份C-的成绩单。考试总共10道大题，至少有一个AI模型把其中六七道做到了基本正确。但这六七道题的解答，没有一个是从头干净到尾的。模型给出的证明里，经常前半段还是极其漂亮的推理，仿佛一个百年难得一遇的天才，后半段突然开始一本正经地胡说八道，把不相关的定理嫁接在一起，或者凭空发明出某个看起来很深奥但查无此论的引理。
评分团队最后只能制定了一个相当“去数学化”的筛沙标准：只要回答里的漏洞是次要的、看起来可以被一个合格的数学家用少量功夫补上，就算通过。这种做法和数学期刊的审稿惯例一脉相承——编辑会在评语里写上“小修后接收”。只不过对AI来说，这些“小修”有时需要人类读懂一颗不按常理出牌的电子大脑里的逻辑。不少答案就趴在这个微妙门槛的边缘，所以到底算六分还是七分，老师们之间也产生了拉扯。
如果非要从这一锅掺杂着极妙和极蠢的浓汤里捞个规律，那就是大语言模型已经具备了两种让数学家羡慕又头疼的能力。第一种是搜刮参考文献。面对一个陌生问题，模型能从文献大海里调出和主题有微弱关联的旧论文，有些引证甚至冷门到连领域内的专家都没听过。这就像一个学生走进图书馆，对着一整面墙的书架，闭着眼睛随手一抽，竟然抽到了一本能提供解题思路的百年前手稿。不过这个学生在接下来的十分钟里，也有可能把那本手稿和一本菜谱混在一起交上来。
模型特别痴迷于琢磨古老的技术工具，把它们拿去试配新的应用场景。比如，遇到某个组合问题时，AI可能搬出一套二十年前物理学家用来处理统计力学计算的配方，磕磕绊绊地往前推。这种“脑中存着所有旧玩具”的做法，有时候真的撞出新玩法，有时候却只是在错误的方向上拼命内卷，产出大量的符号堆砌。改卷人需要小心翼翼地把那些天才的闪光和纯粹的计算垃圾剥离开，难怪他们要抱怨这差事的费心程度。
而那六七道被认可的题目，背后往往藏着另一种戏剧性：答题的AI们采用的策略，有时连出题人自己都从未预想过。问题设计者原本期待的是沿着某个引理笔直走下去，AI却愣是从侧面的灌木丛里蹚出了一条歪歪扭扭但勉强能通的路。不过，灌木丛里多的是枯枝烂叶，模型一边走一边掉渣，留下的推导路径常常需要人类顺着痕迹回去，用重新丈量的方式确认哪些步骤其实是踩在了虚空上。
当然，这场测试最诚实的地方，是它毫不掩饰AI当下在数学上的真实水平天花板。它可能知道几百条定理的编号和内容，也懂得把它们像乐高积木一样拆拼组合，但它对于“证明”这个行为本身的理解仍然极其脆弱。真正成熟的数学研究者会在漫长思考中形成对结构稳定性的直觉，而大语言模型并没有这种判断力——它们对待一个漂亮的构造和一个荒谬的构造，给出的“信心”常常差不太多。所以你能在同一个回答里看到极致老练和极致幼稚的无缝拼接，仿佛一部悬疑小说被撕掉关键章节后胡乱钉在了一起。
C-这个分数之所以刚贴出来就引起讨论，恰恰是因为它既不够好，也不够差。如果所有题目全错，人们可以轻松地说“AI还没懂数学”；如果几乎全对，那将是另一个翻天覆地的故事。现在这种尴尬的中间态，反而给出了最清醒的提示：大型语言模型正在变成一个对数学家有用的研究助手，但这个助手还处在博学又爱编瞎话的阶段。让它去帮忙翻文献、列举已有方法、甚至提出几个看似不搭边的组合想法，它可能比许多人类助理更快；但要让它独立担起严格证明的责任，目前它交上的答卷还足以让改卷老师掉一把头发。
一阶证明团队没有打算停下。既然第一次正式考已经探出了一条公共评测的通道，接下来就是召集更多愿意公开模型的参赛者，以及继续从数学家圈子里征集那种真正有血有肉的问题——不是那种为AI量身定做的人造基准，而是研究者在日常工作中咬着笔杆想破解的真困难。威廉姆斯和同事们相信，只有在这样的真实生态里反复摔打，才能测出一个模型到底是在“学数学”，还是仅仅学会了“学数学的样子”。
而作为远处围观的吃瓜群众，我们或许可以更轻松一点：C-既不是终结，也不是奇迹，它更像个带着噪音的诚实素描。人类数学家有了一位时而聪明绝顶、时而胡话连篇的新同事，接下来拼的是谁能更快学会忍受垃圾，放大那些稀罕的闪光。至于AI会不会有一天改掉乱编的毛病，那是下一轮改卷会上值得再撕几张草稿纸的事了。
热门跟贴