2025年7月，OpenAI用一个大语言模型，在没用到任何数学专用工具的情况下，直接拿下了国际数学奥林匹克竞赛金牌。而在一年前，DeepMind的AlphaProof为了同样的金牌，用掉了几百个TPU天的算力，每个问题还得单独训练两三天。一个连证明步骤都不用检查的通用聊天AI，凭什么打赢专门为数学设计的系统？
专用模型把自己锁死在逻辑链上
AlphaProof的设计思路非常直接。它把数学证明变成一个游戏，每一步必须用Lean语言写出一条合法的推导。这个推导必须通过编译器的检查，不然直接报错。训练数据来自一个专门把自然语言题目翻译成Lean代码的翻译模型，这个翻译模型本身就是基于Gemini改造的。整个系统为了生成足够多的题目变体，动用了上百万道形式化的问题。
这套系统的核心是一个三亿参数的编码器-解码器模型，负责提议下一步该用什么策略。还有一个树搜索算法，负责评估这些策略组合起来能不能走通。为了让模型学会解题，研究者设计了奖励机制，每走一步扣一分，相当于强迫系统找最短路径。
最关键的是，AlphaProof可以通过测试时强化学习来针对特定问题临时补课。针对一道难题，变体生成器会造出几十万道类似的题目，让证明网络在解题过程中继续训练更新权重。换句话说，AlphaProof不是靠自己理解问题本身，而是靠反复刷同类题的变种。论文里写得很清楚，每道题的解决方案需要两到三天测试时强化学习，这说明推理过程本身就需要大量的针对性适应。
纯粹的语言模型没那么多规矩
OpenAI拿金牌的模型没有这些花哨装备。它没有专门的形式化翻译系统，没有变体生成器，也没有树搜索。它就是看自然语言题目，然后用自然语言思考，最后给出答案。连推理过程都是公开的，可以看到模型在想什么。
看GLM 5.1解2024年IMO组合题C4的推理记录，你会发现它的思考过程一点不干净。它在概念空间里跳来跳去，频繁回溯，经常推翻自己刚才的假设，尝试各种高层次的解题方向。有时候它忽然想到一个点子，然后自己又否定掉，过了一会儿又捡回来改一改。这种乱糟糟的思考方式，跟AlphaProof那种步步为营的推进完全相反。
而这个模型的解题能力不止数学。几周之后，同一个模型拿下了国际信息学奥赛金牌，还在AtCoder全球总决赛拿到第二名。这说明它能处理的问题类型远远超出数学，编程竞赛和信息学竞赛本质上都是逻辑推理，但它不需要换一套装备就能上。
哈达马尔的发现流程把一切说透了
1945年，数学家雅克·哈达马尔出版了《数学领域的发明心理学》。他采访了当时最顶尖的数学家和物理学家，包括波利亚、列维-斯特劳斯和爱因斯坦，想搞清楚一个问题：这些最聪明的人是怎么做出新发现的？
结论是，数学发现从来不是纯粹的逻辑推导。
哈达马尔把整个过程分成四个阶段：
- 准备阶段是有意识的，数学家长时间聚焦一个问题，收集资料，试各种办法。
- 酝酿阶段转入潜意识，潜意识接手之后开始大规模搜索，它能把问题看成整体，找到意料之外的连接。
- 启发阶段，潜意识挑中一个满意的方案，突然蹦到意识层面。
- 验证阶段，意识层面才把这个模糊的方案翻译成严谨的数学语言，一步步检查对不对。
最关键的一句话是：严格来说，没有任何发现是纯粹逻辑的。直觉必须从潜意识里冒出来，至少得先启动逻辑工作。
AlphaProof只模拟了准备和验证两个阶段，它干的事情就是一步步搭积木，每一步都得保证搭得稳。但真正关键的酝酿和启发阶段，它压根没有。因为它不允许跳跃，不允许犯错，不允许用模糊的感觉判断一个方向对不对。
语言模型恰好模拟了潜意识的工作方式
LLM在思考的时候，跟哈达马尔描述的潜意识搜索几乎一样。它在自然语言空间里做高层次推理，而不是在Lean验证过的证明空间里做低层次步骤。它可以想一个大概思路，然后用语言描述出来，感觉不对就换一条路。这个过程中很多想法本身就不严谨，但它不在意，因为它知道最后才需要给出一个能通过验证的答案。
这也解释了为什么它能在不同领域都表现不错。哈达马尔指出，发现过程在不同领域是通用的，因为爱因斯坦也在他的采访样本里。只要一个领域最终能用某种方式验证答案，那前面的酝酿和启发阶段就可以共享同一套机制。LLM学会的是怎么在不同概念之间跳跃，怎么用直觉筛选方案，而不是背熟某个特定领域的解题套路。
竞赛比的本来就不是严谨性
回头看AlphaProof和OpenAI模型的对决，有一个根本性的错位：数学竞赛考的是发现能力，不是证明的严谨程度。参赛者需要在有限时间内想出一个从没见过的解法，而不是把一个已知的证明过程一步步写完。
AlphaProof的全部设计都在强调每一步必须正确，它的搜索空间被严格限制在Lean编译器的规则里。这意味着它没法走弯路，没法先错再对，也没法在一个不完整的想法上继续往下推。但真正的数学思考恰恰需要这些不严谨的过程。一个数学家可能在纸上画乱七八糟的图，写一堆不成形的式子，然后才忽然发现那个关键的结构。
语言模型没有这些限制，它的思考记录里可以看到大量被放弃的方向、自相矛盾的推理、以及忽远忽近的联想。这些东西在AlphaProof那里根本不会出现，因为它的系统不允许出现任何不合法的中间状态。
所以问题回到了认知的本质
AlphaProof花了几百个TPU天，外加针对每道题的两三天强化学习，才拿到银牌。而一个不需要形式化证明、不需要变体生成器、不需要树搜索的通用LLM，直接拿了金牌。
这不是算力的问题，也不是算法的问题。AlphaProof从根上就选错了模仿对象，它模仿的是数学家验证答案时的那个意识层面，但数学家真正做出发现靠的是潜意识层面。
那个乱糟糟、不严谨、会走弯路、会自我否定的思考过程，恰恰是发现的关键。LLM的推理痕迹看起来像精神分裂，但正是这种混乱让它能跳出逻辑框架的限制，找到人类数学家都没想到的解法。而AlphaProof那种干净、严谨、步步为营的风格，在竞赛里反而成了致命伤。
验证交给编译器就行，发现得先让脑子飞一会儿。
作者：Chris Hayduk