哈萨比斯预告了人工智能在数学领域的下一场突破用AI生成高难度数学猜想把人类数学家的作用从“发现”推向“验证”。这篇文章从AlphaProof、AlphaGeometry等系统的技术路径讲起分析为什么数学是最适合AI的“封闭测试场”以及为什么说“第37手”只是时间问题。不吹不黑适合关心AI4Science、数学AI和大模型推理能力上限的技术读者阅读。哈萨比斯预告数学的AI“第37手”只剩时间问题最近DeepMind的哈萨比斯又放了一句话数学领域会诞生属于AI的“第37手”。这个说法借用了围棋里“第37手”的典故——AlphaGo在2016年人机大战第37手落子在当时几乎没人预料到事后却被证明是一手开天辟地的好棋。哈萨比斯的言下之意很清楚数学研究中AI也能下出类似的“非人类”妙手而且这个时刻已经不远了。如果你关心AI4Science、大模型推理能力、或数学AI的工程化落地这篇文章比较值得读完。我们不只聊口号而是把AlphaProof、AlphaGeometry这些系统的技术路径拆开看分析它们为什么能解决数学问题、如何落地复现、在普通GPU上能跑到什么程度、以及“AI数学家”还有哪些硬边界。1. 核心能力速览能力项说明代表系统AlphaProof、AlphaGeometry、AlphaTensor、FunSearch核心能力自动证明数学定理、求解几何问题、发现矩阵乘法算法、生成数学猜想适合任务高中数学竞赛题、IMO真题、代数化简、几何构造、算法发现主流方法强化学习 符号推理引擎 大语言模型生成候选步骤硬件需求训练阶段需要大规模TPU/GPU集群推理阶段可在单卡或CPU上验证可复现程度DeepMind未完整开源训练代码但有部分数据集、算法思路和第三方复现本地部署形式多为“LLM生成候选结论 外部符号求解器验证”的流水线接口API能力DeepMind相关模型未直接开放可通过组合开源LLM自行搭建批量任务能力可以批量生成数学猜想或候选证明但需要接入验证器做闭环典型开源替代Lean定理证明器、DeepSeek-R1等推理模型、Wolfram Alpha符号计算从这张表能看到一个关键点所谓的“AI数学突破”并不是一个端到端的魔术而是一条标准流水线——生成候选、符号验证、反馈迭代。这跟市面上的AI编程工具思路很像只是验证器从编译器换成了数学证明系统。2. 为什么数学是AI最容易突破的领域数学一直被看作人类智力的最高象征但站在机器学习角度它反而是最“友好”的测试场。2.1 数学具备完整自动验证器围棋能成为AI突破口是因为规则明确、胜负可判。数学更极端一个定理只要给出严格形式化证明机器就可以自动验证。Lean、Coq、Isabelle这些证明助手已经把“验证”这件事变成了可计算的过程。AI不需要“主观作答”只需要生成一连串证明步骤剩下的交给验证器判定正误。2.2 试错成本极低物理实验要花钱化学实验要耗材医学试验要伦理审批。数学推演纯粹是符号和逻辑操作错了就从头再来成本几乎为零。这让强化学习有了极好的训练环境AI可以自己和自己对弈生成无数候选证明保留成功的丢弃失败的。2.3 结果有客观边界没有“差不多”AI写作文、画图、生成视频好坏很难量化。但数学证明就两种状态证出来了或者没证出来。这种二元反馈让模型训练变得干净利索不需要人工标注好坏只需要验证器给出对错。2.4 搜索空间虽大但有结构数学难题本质上是组合爆炸的搜索问题但数学结构里有大量可用的剪枝信息。AlphaGeometry能解奥数几何题核心不是暴力搜索而是让语言模型学习“辅助点应该加在哪里”把搜索空间压缩到可计算范围。只要找到关键构造后面的证明路径往往会自然展开。3. 核心技术拆解AlphaProof、AlphaGeometry、FunSearch3.1 AlphaProof形式数学与强化学习的结合AlphaProof是DeepMind在IMO 2024中交出的一份答卷。它把大语言模型生成的候选证明步骤接入Lean证明器让模型不断尝试、不断被验证器纠错再用强化学习提升成功率。整个系统更像“推理模型 编译器”的闭环而不是一个单纯的对话式大模型。它做到的成就是在IMO 2024真题中解决了4道题达到银牌水平。虽然离满分还有距离但这个结果对“AI主动提出新数学”来说已经是一个重要信号。3.2 AlphaGeometry把几何题转成可搜索的推理树AlphaGeometry是专攻欧几里得几何的系统。传统几何题的难点在于辅助线、辅助点怎么找。AlphaGeometry的做法是先用大语言模型或预训练网络生成辅助构造再用符号推理引擎类似DG解算器检查这些构造是否通向证明。它的关键洞察在于符号引擎负责穷举推导神经网络负责提出“有希望”的辅助点。前者严谨但迟钝后者灵活但粗放二者结合以后它第一次在IMO几何题上达到了接近人类金牌选手的表现。需要注意一点这套系统并不像ChatGPT那样能和你谈笑风生。你输入一道几何题它返回的是一棵证明树而不是一段自然语言解答。这也正是数学AI和普通AI助手的本质区别。3.3 FunSearch把代码当数学猜想用LLM搜索FunSearch的思路更有意思它不直接搜索数学公式而是让LLM编写一个能生成数学候选结果的程序再由程序自动运行打分把分数反馈给LLM继续迭代。这个方案在面对“极值问题”时表现很好比如上限集问题、装箱问题。本质上FunSearch把“数学发现”转成了“程序合成 进化搜索”。这也是目前可复现性最高的一类方法因为它不依赖专门的证明器只依赖一个能写代码的LLM和一个打分函数。3.4 AlphaTensor从算法层面刷新矩阵乘法AlphaTensor解决的不是证明题而是计算复杂度问题。它把一个“如何用更少乘法完成矩阵相乘”的问题建模为单玩家游戏然后使用强化学习去搜索更优的矩阵乘法分解。结果是它发现了比经典Strassen算法更优的小矩阵乘法方案直接推动算法发现进入自动化时代。从这些系统可以看出数学AI并不是单一模型而是一整套“模型 验证器 搜索策略”的组合。对工程团队来说真正的门槛往往不在深度学习本身而在于如何把数学规则转化成一个可计算、可反馈的闭环系统。4. 本地复现思路用开源LLM搭一个“数学AI流水线”DeepMind的完整系统没有开源但这不代表我们只能围观。用开源大模型也可以搭一条类似“生成-验证-迭代”的数学AI流水线在本地GPU上做实验。4.1 环境准备与硬件建议先看硬件。推荐配置如下实际以本机为准项目最低要求推荐配置GPUNVIDIA 8GB显存NVIDIA 24GB显存CPU8核16核以上内存32GB64GB磁盘80GB200GB NVMe SSD操作系统Ubuntu 22.04 / Windows 11Linux相比文生图、视频生成等任务数学推理模型对显存的要求并不算极端。以DeepSeek-R1系列为例7B量级的模型在8GB显存上可以跑通671B满血版则需要多卡或量化部署。数学任务的瓶颈往往不是“生成答案”而是“验证答案”所以就算没有顶级GPU也可以用CPU跑Lean验证器。4.2 推荐开源模型目前适合数学推理的模型主要有这几类模型优势适合任务DeepSeek-R1系列推理链完整数学推理基准高自然语言数学题、生成候选证明Qwen2.5-Math中文友好数学增强数学题求解、步骤生成LeanDojo的Lean模型面向Lean证明器形式化证明生成通用代码模型DeepSeek-Coder程序搜索FunSearch式程序合成需要注意模型只能“提出步骤”判断对错必须交给验证器。没有验证器的LLM数学对话本质上只是“看起来合理的文字”。4.3 部署一个可用于数学实验的推理服务下面给出一套本地推理服务的通用启动方式适用于绝大多数Ollama可运行的模型。# 安装OllamaLinux/macOS curl -fsSL https://ollama.com/install.sh | sh # 拉取DeepSeek R1 7B量化版 ollama pull deepseek-r1:7b # 启动服务 ollama serve启动后Ollama默认监听11434端口。可以用Python调用import requests url http://127.0.0.1:11434/api/generate payload { model: deepseek-r1:7b, prompt: 请用自然语言证明存在无穷多个质数。, stream: False } resp requests.post(url, jsonpayload, timeout120) print(resp.json()[response])这只是一个对话框服务离AlphaProof还有距离。但它是所有数学AI实验的地基没有生成器后面的一切无从谈起。5. 搭建“生成-验证-迭代”闭环数学AI最小可运行示例5.1 整体架构一条最简数学AI流水线可以用三个模块表示生成器LLM产出一个候选命题或候选证明步骤。验证器符号系统检查该候选是否成立。迭代器如果验证失败把错误信息反馈给LLM重新生成。以“数值数学猜想发现”为例我们可以让LLM提出一个整数序列的递推关系然后用Python验证前N项是否成立。5.2 示例让LLM提出递推公式并用Python验证import requests import sympy as sp def generate_candidate(sequence): prompt f 给定整数序列前6项{sequence} 请提出一个可能的递推公式或通项公式。 只输出公式不要解释。 resp requests.post( http://127.0.0.1:11434/api/generate, json{model: deepseek-r1:7b, prompt: prompt, stream: False}, timeout120 ) return resp.json()[response].strip() seq [1, 1, 2, 3, 5, 8, 13, 21] candidate generate_candidate(seq) print(LLM候选公式:, candidate)5.3 实现验证器并自动反馈def validate(seq, formula_expr): n sp.symbols(n) try: expr sp.sympify(formula_expr) for i, val in enumerate(seq): if sp.simplify(expr.subs(n, i 1)) ! val: return False, f第{i 1}项不匹配期望{val}得到{expr.subs(n, i 1)} return True, 序列前N项验证通过 except Exception as e: return False, f公式解析错误: {e} ok, msg validate(seq, candidate) print(验证结果:, msg)这就是“AI第37手”的最小工程原型先生成再验证失败就迭代。不要小看这个流程AlphaProof的日常训练和它本质相同只是把Python替换成了Lean把序列公式替换成了定理证明项。5.4 用Lean做形式化验证如果想更接近AlphaProof的路线可以安装Lean证明器并让LLM直接生成Lean证明代码。-- 简单验证自然数加法结合律 theorem add_assoc (a b c : Nat) : (a b) c a (b c) : by induction a with | zero simp | succ a ih simp [Nat.add_assoc, ih]这个代码可以被Lean自动检查。如果LLM生成的不是合法证明Lean会返回错误信息。把这个错误信息重新注入提示词就能形成类似AlphaProof的强化学习反馈回路。6. 接口API与批量任务把数学AI变成工程服务6.1 用FastAPI包装推理服务在本地实验成功后可以把推理服务封装成HTTP API。通用写法如下from fastapi import FastAPI from pydantic import BaseModel import requests app FastAPI() class ProveRequest(BaseModel): statement: str app.post(/prove) def prove(req: ProveRequest): ollama_resp requests.post( http://127.0.0.1:11434/api/generate, json{ model: deepseek-r1:7b, prompt: f生成Lean证明代码{req.statement}, stream: False }, timeout300 ) return {candidate: ollama_resp.json()[response]}然后启动服务uvicorn api_server:app --host 0.0.0.0 --port 8000调用curl -X POST http://127.0.0.1:8000/prove \ -H Content-Type: application/json \ -d {statement: 证明两个偶数之和是偶数。}6.2 批量数学命题验证批量任务建议用任务队列简单的做法是先读入命题列表逐个调用验证器把结果写入JSONL文件。注意加上超时和失败重试。import json import requests from tenacity import retry, stop_after_attempt, wait_fixed retry(stopstop_after_attempt(3), waitwait_fixed(2)) def call_llm(prompt): resp requests.post( http://127.0.0.1:11434/api/generate, json{model: deepseek-r1:7b, prompt: prompt, stream: False}, timeout120 ) return resp.json()[response] tasks [ 证明存在无穷多个质数。, 证明根号2是无理数。, 证明所有边相等的三角形是等边三角形。, ] results [] for task in tasks: try: candidate call_llm(task) results.append({task: task, candidate: candidate, status: done}) except Exception as e: results.append({task: task, error: str(e), status: failed}) with open(math_results.jsonl, w, encodingutf-8) as f: for item in results: f.write(json.dumps(item, ensure_asciiFalse) \n)批量任务的核心原则是每一条结果都要可追踪、可重试、可审计。数学AI尤其如此因为生成结果必须和验证结果绑定存储否则无法判断哪条候选真正有效。7. 资源占用与性能观察7.1 显存占用怎么看运行LLM推理时可以用nvidia-smi观察显存占用。以7B量化模型为例在Windows或Linux下单次生成的显存占用通常在6GB到10GB之间实际取决于上下文长度和并发数。如果出现CUDA out of memory优先降低num_ctx或改用更小量化等级。# 实时查看显存 nvidia-smi -l 17.2 生成与验证的瓶颈数学AI流水线的性能瓶颈往往不是GPU而是验证器。LLM生成一段候选证明可能只需要几秒但Lean或符号引擎检查证明可能需要几十秒甚至几分钟。所以在工程上建议把生成服务和验证服务解耦用消息队列异步处理。7.3 如何降低资源占用使用量化模型q4_k_m、q8_0。限制输入输出的最大长度。减少并发请求数。验证任务放到CPUGPU专注生成。批量扫描时不要把过长的失败历史拼进提示词否则上下文会越来越长。8. 常见问题与排查方法问题现象可能原因排查方式解决方案Ollama服务无法访问未启动或端口被占用执行ollama list检查11434端口重启Ollama或监听其他端口模型响应过慢模型过大或GPU显存不足查看nvidia-smi和CPU占用换7B量化模型或限制上下文长度LLM输出大量“解释文字”没有证明代码提示词约束不足查看返回内容格式在提示词中明确“只输出Lean代码”Lean验证失败候选证明不完整查看Lean错误日志将错误信息拼入提示词重新生成Python验证器报Unicode错误模型输出包含非法字符打印原始响应日志清洗输出文本后解析CUDA out of memory显存不足或上下文过长查看推理参数降低batch size、num_ctx或使用CPU推理批量任务卡住某个请求超时无返回添加超时和重试机制用requests timeout和retry策略结果质量不稳定提示词不明确固定few-shot示例每次提供标准输入输出格式9. 最佳实践与使用建议在工程上复现“数学AI”这类系统最容易踩的坑是过度信任LLM生成的自然语言推理。面对数学任务自然语言证明只是“思路草稿”真正可靠的做法是让形式化验证器兜底。建议按下面这套流程推进先用小模型跑通流水线再升级大模型。原始命题、LLM生成结果、验证结果、错误日志全部落盘。每个候选结果都记录模型版本、提示词版本和验证器版本。批量任务必须加超时、重试和并发限制。涉及发表论文或公开成果时必须由数学家复核最终结论不能直接采纳LLM输出。做数学猜想发现时把LLM当“思路生成器”不要当“裁判”。10. 总结与下一步哈萨比斯说的“数学第37手”本质上是说AI会像AlphaGo一样在人类从没想过的地方给出一个反直觉的数学构造或证明路径。AlphaProof、AlphaGeometry、FunSearch已经证明这条路线可行但这些系统目前更像“解题机器”还不是“数学家”。它们能按已有规则搜索和验证却还谈不上自主设定研究纲领。对普通技术人来说这件事离我们并不远。用一台8GB显存的NVIDIA显卡加开源推理模型就已经能搭出“生成-验证-迭代”的数学AI实验环境。真正的价值不在于让AI解几道奥数题而在于建立一套可验证的自动化推理流程——这套流程不仅能用于数学也能迁移到代码验证、合约审计、知识库一致性检查等领域。下一步如果想深入可以先从三件事开始第一用Lean或Python验证器把你手头的问题形式化第二用DeepSeek-R1或Qwen2.5-Math生成候选步骤第三把验证失败的错误信息回灌给模型观察迭代效果。做完这一步你已经比绝大多数只看新闻的人更接近“AI第37手”的真实工作方式。