2016年3月AlphaGo对阵李世石的第二局围棋界记住了第37手。这手棋落在棋盘上时几乎所有人都以为AlphaGo失误了——它偏离了人类对棋理的认知在局部战斗中选择了一个看似笨拙、完全没有“棋形”的位置。但赛后复盘无比清晰这手棋是整盘对局的灵魂它同时防住了黑棋的多种反击在局部交换中逼迫黑棋用一个贴目以上的代价换取实地。古力后来评价这手棋时用了“神仙下凡”四个字。十年后Demis Hassabis正在向外界释放一个更重要的信号数学领域正在接近属于AI的“第37手”。这不再是围棋棋盘上的一步棋而是在数学定理的发现与证明过程中由AI走出一条人类数学家根本不会选择的路径然后被形式化验证为正确。这个“第37手”一旦出现冲击力会远超围棋。因为数学是现代科学的语言也几乎是一切工程系统的底层协议。我对这篇文章的核心判断是数学AI的“第37手”不是一个遥远预言而是一场正在发生的工程事件它的背后恰恰是一套可拆解、可复现的AI工程范式。读者读完这篇文章将能理解Alpha系列数学AI的真实原理、当前边界以及技术开发者可以从哪些具体切口参与这场变革。1. 从AlphaGo第37手说起AI第一次超越人类直觉的瞬间1.1 第37手到底特殊在哪里AlphaGo与李世石的第二局前36手是正常的现代围棋节奏。第37手出现时黑棋正在上方形成势力白棋应该优先处理右边的孤棋或者在左下角定型。AlphaGo却选择在白棋第37手的位置落子——去动一个看起来没有急切性的“未来大场”。这手棋的奥妙在于AlphaGo通过策略网络和价值网络评估出这个点具备极高的“长期胜率预期”而人类棋手给它打出的候选概率极低。后来的变化证明黑棋如果强硬反击会陷入白棋准备好的战斗黑棋如果避让白棋又为右边的战斗储备了足够的弹力。这一手棋的价值被压缩进了一个短期看不出收益、长期却能决定胜负的结构里。换句话说第37手的本质不是“算得更深”而是“评估函数出了问题”——人类职业棋手的直觉评估体系无法为这个局面给出合理的分数。AlphaGo用一套新的价值度量方式无视了人类美学层面的大量噪声。1.2 第37手为什么成为AI叙事的符号这手棋之所以被反复提起是因为它代表了一个转折点AI不再只是“模仿人类高手后超越人类”而是形成了自己的风格AI的决策依据与人类评估体系存在系统性差异但依然可以被客观的规则验证这种差异不是随机的失误而是统计意义上更优的选择。这个结构在数学里恰好能找到一个同构人类数学家的美感、直觉和经验决定了一个猜想值不值得做、一条证明路径值不值得走但AI的搜索系统并不依赖这些主观判断它只关心“在当前证明状态下哪一个动作可以更快逼近可验证的结论”。一旦AI在某个数学问题上走出一个让人类觉得“不符合数学品味”的引理或构造并且最终被证明是正确且高效的那就是数学版的第37手。2. 哈萨比斯为什么说“数学的第37手只剩时间问题”2.1 哈萨比斯在释放什么信号Hassabis在2024年获得诺贝尔化学奖前后多次在公开场合表达过一个观点AI在数学领域取得突破性进展只是时间问题。他从DeepMind的多个项目中看到了这个趋势AlphaFold解决了蛋白质结构预测这是计算生物学里的“第37手”AlphaTensor发现了新的矩阵乘法算法打破了人类维持了数十年的计算复杂度记录AlphaProof在2024年国际数学奥林匹克竞赛中联合AlphaGeometry完成了一道又一道让竞技数学界头疼的题目。从这些轨迹看Hassabis的预告不是营销性质的“造势”而是基于内部实验曲线得出的工程判断。他认为数学是下一个最适合AI“自由发挥”的领域因为数学问题具备两个稀缺属性规则高度明确、结果可以严格验证。2.2 AlphaProof在IMO表现背后的信号据DeepMind官方披露2024年AlphaProof与AlphaGeometry 2组成系统在限定时间内完成了IMO 2024六道题目中的四道达到银牌水平。这个信息让很多人误以为“AI已经能考竞赛数学了”但真正的信号在更深处AlphaProof没有人类解答的“标准答案”可以参考它是在形式化语言Lean中自己搜索证明路径AlphaGeometry 2则通过神经符号混合的方式独立导出了平面几何题的完整证明整个过程采用的是“题目输入 - 自动搜索 - 形式化验证”的流水线中间没有人类干预。这意味着AI已经跨越了“听懂题目”到“写出可验证证明”之间的鸿沟。虽然离“解决黎曼猜想”还很远但工程路径已经走通。2.3 数学第37手的时间表取决于什么如果只评估“AI在竞赛题中拿到奖牌”这个时间差不多已经到了如果评估“AI提出一个人类从未想到、但意义重大的新定理”时间表则取决于三个变量形式化数学语料库的规模和可用性对搜索算法的算力投入数学家与AI系统之间的协作闭环是否成熟。Hassabis判断“只剩时间问题”的核心依据是这三个变量都在指数级改善而这正是工程问题的特征。3. 为什么数学是AI“第37手”最有价值的落点3.1 数学发现的本质是搜索数学家的日常工作大致分为几个环节提出猜想、探索例子、寻找引理、构建证明链条、同行评审。如果把“证明”看成动作序列——每一步选择一个推理规则、一个已有定理、一个辅助构造那么数学证明天然就是一个搜索问题。这个视角意味着数学和围棋一样具备强化学习最需要的结构状态当前证明上下文已知前提、已证明的引理、目标命题动作应用某条定理、做某种情形分析、构造辅助对象反馈证明是否被形式化验证器接受。人类数学家过去靠的是100亿个神经元的先天直觉加成和几十年的训练积累AI则可以用大规模搜索把一个较短直觉链变成超长推理链。3.2 数学问题的可验证性给了AI唯一的安全网围棋的第37手能被认可是因为有最终胜负作为裁判。但数学比围棋更苛刻任何一步错误推演都会让整个证明失效而数学界不允许“这是AI的感觉”这种理由过审。形式化证明系统Lean、Coq、Isabelle提供了一个绝对客观的验证层只有当推理步骤完全符合逻辑规则时系统才接受证明。这让AI可以不依赖人类的主观判断来判定“证明对不对”。这也是数学AI与通用语言模型的最大区别LLM可以编造一个看起来合理的证明但形式化验证器会把这种幻觉挡在门外。数学给AI的“第37手”提供了最终裁判裁判就是逻辑本身。3.3 没有数学的AI体系是不完整的从技术前沿到商业应用几乎所有AI系统都在某个层面依赖数学大模型的注意力机制依赖线性代数和概率论优化器依赖数值分析密码学与区块链依赖数论。如果AI只能在已有数学基础上做工程优化而不能拓展数学边界它的“超级智能”天花板就始终受限。Hassabis预告的本质信号是AI即将成为数学知识的生产者而不只是消费者。这会重塑AI能力的根基。4. 数学与围棋的同构都是“规则简单、搜索空间无穷”的博弈4.1 一套范式两个实例AlphaGo、AlphaZero、AlphaProof、AlphaGeometry这些系统经常被媒体放在一起报道但很少有人指出它们的架构同源性。如果用一张对比表来看会更清晰维度围棋数学定理证明基础规则361个交叉点的落子规则数理逻辑的公理与推理规则状态空间约10的170次方种棋局无穷多个证明上下文动作类型落子应用定理、构造对象、情形分析反馈来源终局胜负形式化验证器人类直觉的盲区局部定式与长期厚势的价值长证明链中某一步的可行替代路径AI切入点策略网络建议候选动作策略网络建议候选推理步骤围棋和数学的共同点是规则空间可以由计算机精确枚举但搜索空间大到无法穷举反馈信号明确且难以伪造。正因如此Alpha系列系统可以在两者之间横跳。4.2 从AlphaZero到AlphaProof自我对弈思想在数学中的迁移AlphaZero的突破在于“自我对弈”不依赖人类棋谱让AI自己与自己下棋通过胜负信号迭代策略。迁移到数学等价于让AI自己提出猜想、自己证明、自己反驳。要实现这种数学“自我对弈”至少有两条路一是“构造-验证对抗”生成器提出一个可能的引理或证明路径验证器返回反例或成功信号两者不断对抗收敛出一个可信的候选定理。二是“命题-证明闭环”AI在某个形式化数学库中随机生成大量真命题然后尝试证明它们并从成功证明中学习模式。用这些模式再去解决更难的问题。AlphaProof训练过程的核心技术细节DeepMind公开得并不完整但从其论文和官方博客透露的信息看它就是在Lean环境中做类似的搜索与自我迭代。围棋是棋盘的博弈数学是逻辑的博弈底层架构本质是同一个。4.3 “第37手”在数学里长什么样如果按围棋第37手的结构类比数学的第37手大概率会是以下几种形式之一一个全新的引理它看起来和问题无关但引入后可以让整个证明链条缩短一半一个出人意料的辅助构造AI在人类不会去探索的对象上找到了联系一条人类认为“不自然”的证明路径比如先证明一个更强的命题再由强命题推出目标命题一个新的数学对象类似AlphaTensor发现的新型矩阵乘法分解。但无论形态如何它都必须通过形式化验证并且足够简洁或普适让人类数学家愿意去理解它背后的原因。哈萨比斯预告的正是这个时刻的到来。5. Alpha系列数学AI的核心技术拆解5.1 总览神经引导 搜索验证我不想让文章停在“AI很厉害”这种观察层面这一节把Alpha系列数学系统的技术架构拆开。目前主流数学AI系统采用“神经引导 搜索验证”的双层结构神经网络LLM或专用策略模型负责提出候选动作比如下一步该应用哪个定理、该尝试哪种情形拆分、该构造什么辅助对象搜索算法最佳优先搜索、蒙特卡洛树搜索或回溯式搜索负责在有限步数内探索候选路径形式化验证器Lean、Coq等提供最终反馈信号判定当前证明是否完整强化学习通过大量自我博弈迭代更新神经网络提高候选动作的“命中率”。在这种架构里神经网络是参谋搜索是冲锋部队验证器是法官。参谋的经验决定了搜索效率法官的判决决定了最终质量。5.2 AlphaProof用强化学习搜索证明AlphaProof的核心流程可以概括为四个步骤将自然语言描述的IMO题目通过训练好的LLM翻译成Lean形式化命题在Lean环境中启动证明搜索神经网络根据当前proof state生成候选策略搜索过程走了大量分支其中大部分失败但成功分支被记录用成功的证明轨迹更新网络权重形成强化学习信号。有一个容易被忽视的细节AlphaProof需要为每道IMO题人工构建形式化后的“问题定义”这个阶段仍然依赖专业人才。真正被AI自动搜索的部分是“从前提推导到结论”的证明过程。5.3 AlphaGeometry神经符号混合的解题路径AlphaGeometry解决平面几何题时采用了另一种混合策略一个符号推理引擎负责执行所有确定性推导规则它逻辑上完备但会陷入组合爆炸一个语言模型负责提出“辅助构造”比如连接两个点、构造中点、延长多条线语言模型缩小了符号引擎的搜索范围符号引擎保证了结果的严格性。这个思路值得做AI工程的开发者学习它把不可解释但灵活的成分语言模型与可验证但僵化的成分符号引擎组合在一起让双方各自发挥优势。做AI Agent时很多人把全部逻辑交给LLM这是不推荐的更稳的架构是LLM负责生成计划、规则引擎负责落地约束。5.4 LLM在数学AI中的三种角色通过Alpha系列系统的架构可以提炼出LLM在数学AI中的三种角色角色输入输出风险翻译者自然语言数学题形式化Lean命题翻译错误导致题目语义漂移搜索者命题与当前proof state候选推理步骤/引理搜索发散、算力消耗高解释者形式化证明人类可读证明梗概总结失真、误导阅读对AI应用开发者来说这三种角色本身就是可复用的Agent设计模式翻译模块负责人机接口搜索模块负责候选生成验证模块负责质量把控。数学AI只是这种模式在逻辑领域的一个特化应用。6. 冷静边界数学AI还不能做什么6.1 从“竞赛题”到“开放问题”的跨度AlphaProof解决IMO题目固然亮眼但IMO题目有一个特性它们已经被证明是可解的且通常存在一个较短的证明路径。这大大降低了搜索难度。黎曼猜想、哥德巴赫猜想、孪生素数猜想这类开放问题没有预先存在的“答案”证明路径可能长达几十上百个关键步骤期间还需要不断提出新的数学对象。从工程角度看这是完全不同的难度等级。6.2 形式化的成本仍然很高AI要形式化证明一个数学命题前提是“形式化本身”已经完成。把自然语言数学知识翻译成Lean可用的定义和定理库需要消耗大量人力。Lean的mathlib社区已经积累了一批库但相对于整个人类数学知识体系覆盖面还很小。这意味着即使AI有能力证明某个新定理如果它的形式化环境没有足够丰富的前提库它也寸步难行。数学AI的价值很大程度取决于形式化基础设施的建设速度。6.3 神经网络幻觉在数学里同样存在LLM在数学推理中照样会产生幻觉。如果让LLM直接写证明它会一本正经地编造一个不存在的引理或者错误引用某条定理。区别在于形式化验证器能识别并拒绝这些幻觉。但这里有个陷阱幻觉进入“候选生成”阶段是无害的因为验证器会过滤如果幻觉出现在“题目翻译”阶段验证器就无法识别——因为Lean命题已经形式化了但可能和原题含义不符。AI数学系统的瓶颈正从推理能力逐步转移到“问题理解与建模”的正确性上。6.4 目前还没有公认的“AI新定理”截至2024年的公开记录还没有出现一个由AI独立提出并经过严谨验证、对数学界产生重大影响的全新定理。AlphaTensor发现的新矩阵乘法算法被视为强信号但它更接近“算法发现”而非“定理发现”。哈萨比斯预告的数学第37手等价于把这个“尚无先例”变成“首次突破”。我的判断是AI最先产生实质贡献的方向会集中在组合数学、离散优化、代数结构和数论中的具体子问题而不是最宏大的千禧年问题。7. 技术开发者如何接住这个信号实操7.1 从“AI数学”到“AI工程”的通用启示作为技术开发者不一定要直接去做数学定理证明但可以从中提取一套可落地的AI工程范式生成器与验证器分离。这套范式适用于代码生成、数据处理、内容审核等多种场景。这里用一个Python演示来展示“验证器兜底”的核心思想AI生成候选结论但最终结论必须通过确定性规则验证。# 文件路径math_agent/candidate_verifier.py from sympy import symbols, expand def verify_identity(candidate: str): x, y symbols(x y) # 将LLM生成的候选恒等式转化为可计算的表达式 # 注意这里只做表达式相等性检查不执行任意代码 expr1 eval(candidate, {__builtins__: {}}, {x: x, y: y}) expr2 (x y) ** 2 return expand(expr1) expand(expr2) # 候选这个恒等式可能是LLM生成的也可能是人工写的 print(verify_identity(x**2 2*x*y y**2))这个例子虽然是教学简化但它揭示了一个工程原则AI负责生成候选规则系统负责裁决有效性。这在很多生产环境中比“完全信任LLM输出”稳健得多。7.2 用数值实验给AI猜想做初筛很多数学问题可以先从数值上找感觉。一个典型的做法是用LLM提出一个关于素数的猜想然后写程序在小范围内枚举验证。下面这个例子实现“哥德巴赫猜想在有限范围内的快速验证”这正是数学AI中“反例搜索哨兵”的迷你版。# 文件路径math_agent/number_siege.py def sieve(n): is_prime [True] * (n 1) is_prime[0] is_prime[1] False for i in range(2, int(n ** 0.5) 1): if is_prime[i]: for j in range(i * i, n 1, i): is_prime[j] False return [i for i in range(n 1) if is_prime[i]] def check_goldbach(limit): primes sieve(limit) prime_set set(primes) for n in range(4, limit, 2): if not any((n - p) in prime_set for p in primes if p n): return n return None print(哥德巴赫猜想在4到100000的偶范围内成立 if check_goldbach(100000) is None else f找到反例: {check_goldbach(100000)})运行这个脚本输出预期是“哥德巴赫猜想在4到100000的偶范围内成立”。这说明数值枚举已经为AI猜想提供了一个可见的“证据墙”。真实的数学AI系统不是靠这种暴力枚举突破难题但“反例搜索”模块是任何数学Agent流水线中不可或缺的部分。7.3 搭建一个“猜想-验证”Agent的最小骨架如果是有一定AI工程经验的开发者可以直接尝试搭建一个“LLM生成猜想 自动验证”的闭环。下面是一个通用的Agent骨架不绑定特定API服务商重点展示控制流。# 文件路径math_agent/conjecture_agent.py import requests def llm_generate_conjecture(domain_desc: str) - str: # 实际使用时替换为自己的LLM服务地址与鉴权参数 resp requests.post( https://api.example.com/v1/chat/completions, json{ messages: [ {role: system, content: 你是一个数学研究助手。}, {role: user, content: f在{domain_desc}范围内观察数值规律提出一个可验证的猜想。} ], temperature: 0.2 }, timeout30 ) return resp.json()[choices][0][message][content] def deterministic_verifier(conjecture: str) - bool: # 在这里把自然语言猜想映射为可执行检查函数略 # 核心原则验证器不能使用LLM必须使用确定性代码或符号引擎 return False if __name__ __main__: desc 素数 p 大于3时p^2 - 1 整除规律 conjecture_text llm_generate_conjecture(desc) print(候选猜想:, conjecture_text) passed deterministic_verifier(conjecture_text) print(验证结果:, 通过 if passed else 未通过保留记录待人工检查)这段代码的重点不是“能直接解决数学难题”而是展示一个工程上正确的流程LLM负责发散生成确定性验证器负责收敛判定。生产级数学Agent还需要考虑缓存、失败重试、验证器回滚、审计日志等因素。7.4 真正接触数学AI的硬核路线形式化证明如果想让自己的职业方向贴近哈萨比斯预告的领域最值得投入的是形式化证明技术。Lean 4是当前数学形式化社区使用较广的工具配合mathlib库已经能够处理大量现代数学命题。以当前主流版本为例安装Lean 4并新建一个Lake项目后可以尝试写下最小证明import Mathlib example : 2 2 4 : by norm_num在Lean项目环境中运行验证器会给出“该命题已证明”的反馈。这个简单的示例背后是数学AI最依赖的机制由计算机检查每一步推理而不是由人类判断证明是否正确。从学习路径看建议先熟悉Lean的证明策略语法rfl、norm_num、intro、apply、exact等再尝试给数学库提交一个小证明。掌握形式化证明的人在未来既是数学家与AI之间的翻译者也是验证基础设施的工程主力。8. AI数学带来的工程机会与生态变化8.1 形式化验证工具链的需求上升数学模型要想被AI可靠地使用首先必须做到“可机器验证”。因此Lean、Coq、Isabelle等证明助手的工程化水平会直接影响AI数学的发展速度。围绕这些工具会产生大量基础设施需求将数学论文自动翻译为形式化语言的辅助工具数学库的搜索与检索系统证明状态的可视化调试器面向数学家的低门槛形式化SDK。这些方向几乎都是“AI工程 编程语言 数学知识”的交叉岗位目前人才供给很少。8.2 数学Agent平台与工具链从AI应用开发角度数学Agent不只是“自动解题”它会演化成一套完整的工具链模块功能类似工程组件问题理解解析自然语言/LaTeX数学表达式NER、文档解析、LLM猜想生成基于数据与过去证明Suggest新命题多Agent生成器、数据引擎证明搜索在形式化环境中搜索路径搜索服务、调度器验证执行调用Lean等验证器CI、测试框架结果解释把形式化证明转换成人类可读文本LLM摘要、文档生成这套结构与现代软件开发中的“需求解析-代码生成-自动化测试-文档生成”几乎完全一致。数学AI的工程实践本质上是在更严格的逻辑约束下做Agent编排。8.3 数学与机器学习在工具层面的融合进一步看数学AI的成熟会反哺AI产业本身自动发现新的损失函数或优化算法对现有算法做形式化复杂度证明自动生成训练数据的合成逻辑在模型推理过程中引入数学规则约束减少幻觉。哈萨比斯说数学第37手“只剩时间问题”对技术开发者的真实含义是掌握“神经网络 确定性验证”这套混合架构可能比等待一个“超级数学家AI模型”的出现更实际。8.4 风险与责任数学AI同样存在风险。如果AI大规模生成表面上正确的伪证明而验证器覆盖不足会污染学术生态。因此AI数学系统必须默认接入形式化验证并保留完整的审计与回溯能力。这个领域也应当保持适度的开源合作让验证器、数据、模型权重经过可重复的版本管理避免少数机构的黑箱系统垄断数学发现。9. 总结与后续学习路径回到第37手。AlphaGo那一步棋之所以被铭记不是因为它显示了“算力有多强”而是因为它在人类以为已经接近真理的领域里找到了一条全新的路径。数学领域如果出现第37手意义会彻底不同它说明机器可以成为数学知识的发现者而不只是计算工具。我的最终判断是未来两到三年AI数学领域的首个独立定理发现会来自某个局部子问题届时的技术关键词大概率是“强化学习 形式化验证 领域专用数据”。这件事既不会像科幻电影一样一夜爆发也不会永远停滞。对技术开发者来说最值得做的不是等那个消息出来而是提前掌握三件事学习Lean或其他形式化证明系统的工程用法哪怕只做小例子理解“神经生成 确定性验证”的Agent架构在自己的业务场景里尝试落地关注DeepMind、OpenAI等机构发布的数学AI系统及其训练数据构建方式那会是最新工程经验的来源。数学的“第37手”正在逼近。当它真正出现时懂工程、懂逻辑、懂验证的人不会只是旁观者。