数学研究曾经被看作一个少数天才驱动的领域欧拉、高斯、伽罗瓦、拉马努金这样的名字通常和一两个划时代定理绑定。但进入 21 世纪后数学证明的复杂度已经远远超出单人脑力的极限——从单篇论文几百页的密度到计算机辅助证明逐渐成为常态。AI 的出现尤其是大语言模型、符号计算系统和交互式证明助手的组合正在终结这个依赖“个体直觉灵光一现”的英雄时代。本文要讨论的不是“AI 会不会取代数学家”而是“AI 如何把数学研究从孤胆天才模式变成人类与多个 AI 工具协作验证的世界思维模式”并给出一套可以立刻上手的最小工作流用大模型生成数学推导用 SymPy 做符号验证再用 Lean 4 做形式化证明检查。这套工作流并不复杂但它非常真实地反映了当下 AI 数学实践的核心原则大模型负责提出假设和草稿符号计算负责精确运算证明器负责把每一个结论变成机器可检查的证明。文章会从概念、环境、代码、验证、排错到生产化扩展逐步展开读者可以照着一行一行跑通。1. 数学为什么需要告别“英雄时代”1.1 从个体天才到协作系统的现实原因过去数学发现的核心动力确实来自个人天才。拉马努金可以写下大量未经证明的恒等式欧拉能凭直觉猜出很多级数结果但这种模式有几个前提数学分支相对少、问题相对集中、证明的长度和复杂度有限。当代数学的现状完全不同。一个突出的例子是近代数学中某些大型定理的证明比如有限单群分类横跨数十位数学家、数百篇论文、累计上万页。单个天才已经不可能掌握所有细节。另一个例子是 Kepler 猜想虽然最终由 Hales 用计算机辅助证明完成但证明过程本身因为太长和太复杂人类评审几乎无法完全复核。AI 要参与的正是这个环节它不像数学家在黑板上推公式而是作为一个“批量生成假设并快速验证”的引擎配合符号计算和证明器给出可信结果。这既不是取代数学家也不是把一切交给黑盒而是把数学研究的链条拆成多个可信组件。1.2 大模型、符号计算与证明助手的分工在落地之前先分清三类工具因为很多 AI 数学项目失败是因为角色混淆大语言模型LLM擅长自然语言理解、模式联想、草稿生成不擅长精确计算和可靠证明。符号计算系统SymPy、Mathematica、Maple擅长按照确定算法完成求导、积分、化简、方程求解结果可复现但不具备探索性。交互式定理证明器Lean、Coq、Isabelle擅长把数学命题转化为机器可检查的形式化证明证明一旦被内核接受就等同于绝对可靠的逻辑结论。从能力边界看LLM 负责“想”SymPy 负责“算”Lean 负责“证”。三者的组合正好覆盖数学研究中最容易出错的三个环节推导方向、代数运算、逻辑严谨性。1.3 为什么说 AI 会终结“英雄时代”如果把“英雄时代”理解为“某个人的灵感和直觉决定数学进步的速度”那么 AI 确实正在终结它。原因很直接数学发现过程开始变成可批量执行的工程提出猜想、用符号计算测试、用证明器检查。个人与个人之间的差距被工具抹平。有了好的工具链一个普通研究者也能验证复杂猜想而即使是最聪明的数学家也无法在不做形式化的情况下保证上千行推导无错。验证能力从“评审专家读论文”变成“机器跑证明”。这改变了“什么算一个结论成立”的标准。所以这里的“世界思维”并不是指一个超级 AI 拥有全人类的数学知识而是指由人类、多个 AI 模型、符号计算工具、证明器组成的分布式认知网络。每一个节点都不可全信但通过明确分工和互相验证整个系统可以产生远远超过单个天才的可靠成果。2. 环境准备搭建一个可运行的 AI 数学工作台要亲手跑通“LLM SymPy Lean”的最小闭环建议先准备以下环境。如果暂时无法安装 Lean也可以先跳过只跑通前两部分。2.1 环境清单组件作用学习环境建议生产环境建议Python 3.9运行脚本和符号验证3.10 即可3.11固定版本SymPy符号计算与结果校验最新稳定版锁版本配合 CIOllama 或任意 OpenAI 兼容服务调用大模型生成数学推导Ollama 7B 数学模型API 网关支持多模型路由Lean 4 Mathlib形式化证明检查可安装 Lean 4 和 Mathlib作为独立服务或 CI 任务Jupyter Notebook 或 VS Code交互式开发可选不建议生产依赖2.2 安装 Python 依赖在终端里创建虚拟环境并安装 SymPy 和 requestspython -m venv venv source venv/bin/activate # Windows 下使用 venv\Scripts\activate pip install sympy requests验证 SymPy 是否安装成功python -c import sympy; print(sympy.__version__)这里使用requests是为了直接调用 Ollama 的 OpenAI 兼容接口避免引入大型 SDK代码更透明。2.3 本地启动一个数学大模型Ollama 是一个常见的本地大模型运行工具。安装完成后建议拉取一个数学能力较好的模型例如qwen2.5-math:7b。如果硬件内存有限可以改用qwen2.5-math:1.5b效果会差一些但流程一致。ollama pull qwen2.5-math:7b ollama list启动服务后默认监听http://localhost:11434。这个地址可以作为后续代码里的base_url。如果读者已经有其他 OpenAI 兼容服务比如企业内部网关也用同样的方式接入。OpenAI 兼容协议的好处是只需要改base_url、api_key、model三个参数其余代码不用变。注意本地模型提供的数学能力通常弱于云端旗舰模型但优点是不涉及密钥、隐私边界清晰、便于在自动化流程中反复调用。真正进入生产时应把模型调用抽象成服务而不是在业务代码里直接拼连接。2.4 安装 Lean 4可选但推荐Lean 4 是微软研究院推出的交互式定理证明器。建议使用elan安装curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | shWindows 用户可以直接从 Lean 官网下载安装包。安装完成后创建一个 Lean 项目并引入 Mathliblake new math-check cd math-check lake update如果网络不稳定也可以暂时不做这一步只阅读后续节选的 Lean 代码理解形式化证明的语义。3. 核心流程让大模型生成推导再用 SymPy 验证这个最小工作流的核心思路很简单大模型输出一个数学表达式SymPy 负责计算标准答案然后把两者做符号化简比较。只有化简差为零才认为通过。3.1 封装一个统一的 LLM 调用函数为了不让业务代码被模型供应商绑定写一个ask_llm函数使用 OpenAI 兼容的 HTTP 接口。下面示例默认使用本地 Ollamaimport requests def ask_llm(prompt: str, model: str qwen2.5-math:7b, base_url: str http://localhost:11434/v1, temperature: float 0.1) - str: url f{base_url}/chat/completions payload { model: model, messages: [{role: user, content: prompt}], temperature: temperature, max_tokens: 2048, stream: False } resp requests.post(url, jsonpayload, timeout120) resp.raise_for_status() return resp.json()[choices][0][message][content].strip()几个参数需要解释temperature设置为 0.1 或更低。数学推理需要确定性和可复现性温度偏高会导致每次结果都不一样给验证环节带来额外成本。max_tokens数学推导可能比较长2000 到 4096 比较合适。过短会导致输出被截断表达式残缺。base_url需要带/v1前缀因为 Ollama 暴露的是 OpenAI 兼容接口。3.2 用导数作为第一个验证案例在数学中求导规则明确适合作为语法验证。比如计算f(x) sqrt(x^2 1)的导数。先定义 SymPy 变量和参考答案import sympy as sp x sp.Symbol(x) f sp.sqrt(x**2 1) expected sp.diff(f, x) print(Expected derivative:, sp.simplify(expected))这里sp.diff会得到x/sqrt(x**2 1)。然后要求大模型输出同样格式的 SymPy 表达式function_str sqrt(x**2 1) prompt ( 你是专业数学助手。请用 Python/SymPy 兼容格式 f求函数 f(x) {function_str} 的导数。 只输出一个表达式不要解释不要输出其他文字。 ) llm_output ask_llm(prompt) print(LLM output:, llm_output) try: llm_expr sp.sympify(llm_output) diff_result sp.simplify(llm_expr - expected) is_correct diff_result 0 print(Is correct:, is_correct) except Exception as e: print(Parse or compare failed:, e) is_correct False关键在于sp.simplify(llm_expr - expected)。两个表达式可能在形式上不同比如x*(x^21)^(-1/2)和x/sqrt(x^21)直接会返回False因此必须做化简差比较。3.3 扩展到积分场景积分比求导更容易出现结果形式差异。可以换成以下问题function_str x * exp(x) * sin(x) prompt ( 请用 Python/SymPy 兼容格式 f计算不定积分 ∫ {function_str} dx。 只输出表达式不要解释。 ) llm_output ask_llm(prompt) expected_integral sp.integrate(x * sp.exp(x) * sp.sin(x), x) llm_expr sp.sympify(llm_output) diff sp.simplify(llm_expr - expected_integral) print(Expected:, expected_integral) print(LLM:, llm_expr) print(Pass:, diff 0)这个积分结果是x*exp(x)*sin(x)/2 - x*exp(x)*cos(x)/2 - exp(x)*sin(x)/2 ...不同模型可能给出带常数的不同形式。化简通常能消除差别。3.4 符号计算不能永远信任sp.simplify在很多情况下有效但它本身是启发式算法。如果遇到复杂嵌套根式、三角函数或特殊函数化简可能超时或无法抵消所有项。因此SymPy 验证不能替代形式化证明只适合作为第一层快速检查。4. 把结论变成机器可验证的证明Lean 4 最小示例SymPy 验证的意义在于“结果在数值和符号上去除了常见错误”但它并不能证明“这个表达式对任意定义的变量都成立”。Lean 4 这类证明器能把数学命题变成逻辑内核检查的证明项每一条推理都必须经过规则允许。4.1 为什么需要证明器大模型输出的公式即使经过 SymPy 验证也只是说明“在某个计算过程中两边相等”。真实数学研究往往涉及条件、定义、公理而这些在大模型中是无法被严格表述的。Lean 4 可以做到每个证明步骤都会被内核检查。只能使用给定公理和已定义策略不能依赖直觉。证明结果可导出为可信计算产物。4.2 Lean 代码示例假设要证明一个简单的代数恒等式import Mathlib.Data.Real.Basic example (x : ℝ) : x^2 2*x 1 (x1)^2 : by ring这段代码的含义是对于任意实数x证明x^2 2*x 1等于(x1)^2。策略ring会展开计算并构造一个完整证明项。更接近数学推理的例子import Mathlib example (a b : ℝ) (h : a b 0) : (a b)^2 0 : by rw [h] ring这里的rw [h]把ab替换为0然后ring证明0^20。实际研究中证明器更多用来检查一长串数学推导的跳步是否合法。对于大模型生成的高层证明思路数学家可以用 Lean 把主要引理逐条形式化。4.3 为什么大模型无法替代证明器不严谨地说大模型是在做“模式联想”它擅长从训练语料里复现类似证明的结构但不保证每一步都符合逻辑规则。证明器则相反它不强求创新只要进入内核每个步骤都必须严格通过类型检查。把两者结合可以让大模型负责找到证明路径而证明器负责验证路径是否真的连通。5. 常见问题与排查链路实际跑这套流程时大概率会遇到下面这些问题。按“现象 - 原因 - 排查 - 解决”的顺序整理成表格方便直接对照。现象常见原因检查方式处理建议LLM 输出大量解释文字SymPy 解析失败提示词没有限制输出格式打印llm_output查看在提示词里写明“只输出一个表达式不要解释”或程序里做后处理表达式包含 LaTeX 命令sympify报错模型仍然使用了 LaTeX检查输出是否含\frac、\sqrt给模型示例输出要求使用Python风格或先写一个 LaTeX 解析层计算结果数学上相等但simplify 0返回 False表达式形式复杂SymPy 化简不彻底尝试sp.trigsimp,sp.expand,sp.apart使用sp.simplify后仍不通过再尝试多次变换或者手工检查关键项本地 Ollama 调用超时模型过大或首次加载慢查看 Ollama 日志CPU/GPU 占用换更小模型增加timeout提前做一次预热调用Lean 项目编译非常慢Mathlib 体积庞大观察编译日志第一次编译耐心等待不要在每次运行都重建使用lake env增量构建大模型对同一个问题多次回答不一致temperature 设置过高多跑几次看方差将 temperature 降到 0 或 0.1在业务层增加缓存符号计算内存爆满或卡死表达式太长或化简太激进观察 CPU 和内存先sp.expand替代sp.simplify限制表达式长度分段验证排查顺序建议先看模型输出原文再确认 SymPy 解析是否成功再看化简结果是否真的为零。大多数失败都在前两层不要一上来就怀疑证明器或数学理论。6. 从实验脚本走向生产级“世界思维”6.1 设计项目结构实验脚本可以随便写但生产环境需要把“调用模型”和“数学验证”解耦。推荐结构math-ai-workbench/ ├── config.yaml ├── main.py ├── llm_client.py ├── validator.py ├── lean_check/ # Lean 项目 │ ├── lakefile.lean │ └── Mathlib.lean ├── tests/ │ ├── test_validator.py │ └── cases.json └── requirements.txt6.2 配置外置化把模型名称、接口地址、温度、超时时间放到config.yamlllm: base_url: http://localhost:11434/v1 model: qwen2.5-math:7b temperature: 0.1 timeout: 120 validation: max_expr_len: 1000 simplify_timeout: 10 check_constant_equivalence: true加载配置时使用PyYAMLpip install pyyamlimport yaml with open(config.yaml, r, encodingutf-8) as f: config yaml.safe_load(f)这样切换本地模型、云端模型或内部网关时不需要改代码。6.3 增加日志和缓存在生产环境每一条“AI 生成 - 符号验证 - 证明器检查”的链路都应当留下记录。import logging import hashlib import json logger logging.getLogger(math_ai) logger.setLevel(logging.INFO) def make_cache_key(user_question: str, model: str) - str: payload json.dumps({q: user_question, m: model}, ensure_asciiFalse) return hashlib.sha256(payload.encode()).hexdigest()缓存可以用简单的 JSON 文件也可以使用 Redis。缓存的意义不只是省钱更是让同样的数学问题在相同模型配置下得到确定性结果便于回归测试。6.4 建立验证回归测试集把一组已知正确答案的题目放到cases.json中[ { question: sqrt(x**2 1) 的导数, func: sqrt(x**2 1), operation: diff, expected_kind: derivative }, { question: ∫ x*exp(x)*sin(x) dx, func: x*exp(x)*sin(x), operation: integrate, expected_kind: antiderivative } ]然后在tests/test_validator.py里写一个简单的回归测试import sympy as sp def test_derivative_cases(): x sp.Symbol(x) cases [ (sqrt(x**2 1), x / sp.sqrt(x**2 1)), (sin(x)*exp(x), sp.diff(sp.sin(x) * sp.exp(x), x)) ] for func_str, expected in cases: expr sp.sympify(func_str) actual sp.diff(expr, x) assert sp.simplify(actual - expected) 0这里不依赖 LLM只验证 SymPy 自身逻辑确保验证层本身不坏。再写一层 mock LLM 的测试模拟大模型输出验证主流程是否正确。6.5 学习环境与生产环境的差异维度学习环境生产环境模型本地小模型即可选数学微调模型或旗舰模型做评测选型验证SymPy 结果人工看一眼即可必须自动回归且引入 Lean/Coq超时默认 120 秒要分任务设置简单推导 30 秒复杂证明 10 分钟以上异常处理try except直接跳过必须有重试、降级、告警、人工复核通道安全本地运行没有密钥泄露风险密钥必须托管在密钥管理服务中可追溯只看最终输出保存 LLM 原始输出、模型版本、验证日志、证明文件版本6.6 实际项目中最重要的三条建议第一永远不要让大模型直接写最终证明结论。大模型适合生成草稿验证工作必须交给确定性的计算工具和证明器。第二不要急于把整个数学研究流程自动化。先把单个步骤的验证闭环跑通再扩展到多步推理最后再讨论“自主数学 Agent”。第三每一步的输入输出都要规范化尤其是数学表达式格式。LLM 输出自由文本程序只接受格式严格的表达式中间必须有清洗和解析层否则验证本身就会成为新的错误来源。现在这个最小工作流已经足以覆盖大模型生成求导或积分结果SymPy 进行符号验证Lean 对关键恒等式做形式化证明。在它之上进一步扩展可以加入多步推理任务拆分、数学 Agent 的记忆模块、多个模型投票、证明库自动搜索等功能。那个目标是“世界思维”但每一步都仍然要建立在可验证的工程基础之上。数学的“英雄时代”终结之后取而代之的不是某一个超级 AI而是一个由工具、数据和纪律构成的协作系统。 大模型、符号计算与证明助手：AI重塑数学研究协作方式
数学研究曾经被看作一个少数天才驱动的领域欧拉、高斯、伽罗瓦、拉马努金这样的名字通常和一两个划时代定理绑定。但进入 21 世纪后数学证明的复杂度已经远远超出单人脑力的极限——从单篇论文几百页的密度到计算机辅助证明逐渐成为常态。AI 的出现尤其是大语言模型、符号计算系统和交互式证明助手的组合正在终结这个依赖“个体直觉灵光一现”的英雄时代。本文要讨论的不是“AI 会不会取代数学家”而是“AI 如何把数学研究从孤胆天才模式变成人类与多个 AI 工具协作验证的世界思维模式”并给出一套可以立刻上手的最小工作流用大模型生成数学推导用 SymPy 做符号验证再用 Lean 4 做形式化证明检查。这套工作流并不复杂但它非常真实地反映了当下 AI 数学实践的核心原则大模型负责提出假设和草稿符号计算负责精确运算证明器负责把每一个结论变成机器可检查的证明。文章会从概念、环境、代码、验证、排错到生产化扩展逐步展开读者可以照着一行一行跑通。1. 数学为什么需要告别“英雄时代”1.1 从个体天才到协作系统的现实原因过去数学发现的核心动力确实来自个人天才。拉马努金可以写下大量未经证明的恒等式欧拉能凭直觉猜出很多级数结果但这种模式有几个前提数学分支相对少、问题相对集中、证明的长度和复杂度有限。当代数学的现状完全不同。一个突出的例子是近代数学中某些大型定理的证明比如有限单群分类横跨数十位数学家、数百篇论文、累计上万页。单个天才已经不可能掌握所有细节。另一个例子是 Kepler 猜想虽然最终由 Hales 用计算机辅助证明完成但证明过程本身因为太长和太复杂人类评审几乎无法完全复核。AI 要参与的正是这个环节它不像数学家在黑板上推公式而是作为一个“批量生成假设并快速验证”的引擎配合符号计算和证明器给出可信结果。这既不是取代数学家也不是把一切交给黑盒而是把数学研究的链条拆成多个可信组件。1.2 大模型、符号计算与证明助手的分工在落地之前先分清三类工具因为很多 AI 数学项目失败是因为角色混淆大语言模型LLM擅长自然语言理解、模式联想、草稿生成不擅长精确计算和可靠证明。符号计算系统SymPy、Mathematica、Maple擅长按照确定算法完成求导、积分、化简、方程求解结果可复现但不具备探索性。交互式定理证明器Lean、Coq、Isabelle擅长把数学命题转化为机器可检查的形式化证明证明一旦被内核接受就等同于绝对可靠的逻辑结论。从能力边界看LLM 负责“想”SymPy 负责“算”Lean 负责“证”。三者的组合正好覆盖数学研究中最容易出错的三个环节推导方向、代数运算、逻辑严谨性。1.3 为什么说 AI 会终结“英雄时代”如果把“英雄时代”理解为“某个人的灵感和直觉决定数学进步的速度”那么 AI 确实正在终结它。原因很直接数学发现过程开始变成可批量执行的工程提出猜想、用符号计算测试、用证明器检查。个人与个人之间的差距被工具抹平。有了好的工具链一个普通研究者也能验证复杂猜想而即使是最聪明的数学家也无法在不做形式化的情况下保证上千行推导无错。验证能力从“评审专家读论文”变成“机器跑证明”。这改变了“什么算一个结论成立”的标准。所以这里的“世界思维”并不是指一个超级 AI 拥有全人类的数学知识而是指由人类、多个 AI 模型、符号计算工具、证明器组成的分布式认知网络。每一个节点都不可全信但通过明确分工和互相验证整个系统可以产生远远超过单个天才的可靠成果。2. 环境准备搭建一个可运行的 AI 数学工作台要亲手跑通“LLM SymPy Lean”的最小闭环建议先准备以下环境。如果暂时无法安装 Lean也可以先跳过只跑通前两部分。2.1 环境清单组件作用学习环境建议生产环境建议Python 3.9运行脚本和符号验证3.10 即可3.11固定版本SymPy符号计算与结果校验最新稳定版锁版本配合 CIOllama 或任意 OpenAI 兼容服务调用大模型生成数学推导Ollama 7B 数学模型API 网关支持多模型路由Lean 4 Mathlib形式化证明检查可安装 Lean 4 和 Mathlib作为独立服务或 CI 任务Jupyter Notebook 或 VS Code交互式开发可选不建议生产依赖2.2 安装 Python 依赖在终端里创建虚拟环境并安装 SymPy 和 requestspython -m venv venv source venv/bin/activate # Windows 下使用 venv\Scripts\activate pip install sympy requests验证 SymPy 是否安装成功python -c import sympy; print(sympy.__version__)这里使用requests是为了直接调用 Ollama 的 OpenAI 兼容接口避免引入大型 SDK代码更透明。2.3 本地启动一个数学大模型Ollama 是一个常见的本地大模型运行工具。安装完成后建议拉取一个数学能力较好的模型例如qwen2.5-math:7b。如果硬件内存有限可以改用qwen2.5-math:1.5b效果会差一些但流程一致。ollama pull qwen2.5-math:7b ollama list启动服务后默认监听http://localhost:11434。这个地址可以作为后续代码里的base_url。如果读者已经有其他 OpenAI 兼容服务比如企业内部网关也用同样的方式接入。OpenAI 兼容协议的好处是只需要改base_url、api_key、model三个参数其余代码不用变。注意本地模型提供的数学能力通常弱于云端旗舰模型但优点是不涉及密钥、隐私边界清晰、便于在自动化流程中反复调用。真正进入生产时应把模型调用抽象成服务而不是在业务代码里直接拼连接。2.4 安装 Lean 4可选但推荐Lean 4 是微软研究院推出的交互式定理证明器。建议使用elan安装curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | shWindows 用户可以直接从 Lean 官网下载安装包。安装完成后创建一个 Lean 项目并引入 Mathliblake new math-check cd math-check lake update如果网络不稳定也可以暂时不做这一步只阅读后续节选的 Lean 代码理解形式化证明的语义。3. 核心流程让大模型生成推导再用 SymPy 验证这个最小工作流的核心思路很简单大模型输出一个数学表达式SymPy 负责计算标准答案然后把两者做符号化简比较。只有化简差为零才认为通过。3.1 封装一个统一的 LLM 调用函数为了不让业务代码被模型供应商绑定写一个ask_llm函数使用 OpenAI 兼容的 HTTP 接口。下面示例默认使用本地 Ollamaimport requests def ask_llm(prompt: str, model: str qwen2.5-math:7b, base_url: str http://localhost:11434/v1, temperature: float 0.1) - str: url f{base_url}/chat/completions payload { model: model, messages: [{role: user, content: prompt}], temperature: temperature, max_tokens: 2048, stream: False } resp requests.post(url, jsonpayload, timeout120) resp.raise_for_status() return resp.json()[choices][0][message][content].strip()几个参数需要解释temperature设置为 0.1 或更低。数学推理需要确定性和可复现性温度偏高会导致每次结果都不一样给验证环节带来额外成本。max_tokens数学推导可能比较长2000 到 4096 比较合适。过短会导致输出被截断表达式残缺。base_url需要带/v1前缀因为 Ollama 暴露的是 OpenAI 兼容接口。3.2 用导数作为第一个验证案例在数学中求导规则明确适合作为语法验证。比如计算f(x) sqrt(x^2 1)的导数。先定义 SymPy 变量和参考答案import sympy as sp x sp.Symbol(x) f sp.sqrt(x**2 1) expected sp.diff(f, x) print(Expected derivative:, sp.simplify(expected))这里sp.diff会得到x/sqrt(x**2 1)。然后要求大模型输出同样格式的 SymPy 表达式function_str sqrt(x**2 1) prompt ( 你是专业数学助手。请用 Python/SymPy 兼容格式 f求函数 f(x) {function_str} 的导数。 只输出一个表达式不要解释不要输出其他文字。 ) llm_output ask_llm(prompt) print(LLM output:, llm_output) try: llm_expr sp.sympify(llm_output) diff_result sp.simplify(llm_expr - expected) is_correct diff_result 0 print(Is correct:, is_correct) except Exception as e: print(Parse or compare failed:, e) is_correct False关键在于sp.simplify(llm_expr - expected)。两个表达式可能在形式上不同比如x*(x^21)^(-1/2)和x/sqrt(x^21)直接会返回False因此必须做化简差比较。3.3 扩展到积分场景积分比求导更容易出现结果形式差异。可以换成以下问题function_str x * exp(x) * sin(x) prompt ( 请用 Python/SymPy 兼容格式 f计算不定积分 ∫ {function_str} dx。 只输出表达式不要解释。 ) llm_output ask_llm(prompt) expected_integral sp.integrate(x * sp.exp(x) * sp.sin(x), x) llm_expr sp.sympify(llm_output) diff sp.simplify(llm_expr - expected_integral) print(Expected:, expected_integral) print(LLM:, llm_expr) print(Pass:, diff 0)这个积分结果是x*exp(x)*sin(x)/2 - x*exp(x)*cos(x)/2 - exp(x)*sin(x)/2 ...不同模型可能给出带常数的不同形式。化简通常能消除差别。3.4 符号计算不能永远信任sp.simplify在很多情况下有效但它本身是启发式算法。如果遇到复杂嵌套根式、三角函数或特殊函数化简可能超时或无法抵消所有项。因此SymPy 验证不能替代形式化证明只适合作为第一层快速检查。4. 把结论变成机器可验证的证明Lean 4 最小示例SymPy 验证的意义在于“结果在数值和符号上去除了常见错误”但它并不能证明“这个表达式对任意定义的变量都成立”。Lean 4 这类证明器能把数学命题变成逻辑内核检查的证明项每一条推理都必须经过规则允许。4.1 为什么需要证明器大模型输出的公式即使经过 SymPy 验证也只是说明“在某个计算过程中两边相等”。真实数学研究往往涉及条件、定义、公理而这些在大模型中是无法被严格表述的。Lean 4 可以做到每个证明步骤都会被内核检查。只能使用给定公理和已定义策略不能依赖直觉。证明结果可导出为可信计算产物。4.2 Lean 代码示例假设要证明一个简单的代数恒等式import Mathlib.Data.Real.Basic example (x : ℝ) : x^2 2*x 1 (x1)^2 : by ring这段代码的含义是对于任意实数x证明x^2 2*x 1等于(x1)^2。策略ring会展开计算并构造一个完整证明项。更接近数学推理的例子import Mathlib example (a b : ℝ) (h : a b 0) : (a b)^2 0 : by rw [h] ring这里的rw [h]把ab替换为0然后ring证明0^20。实际研究中证明器更多用来检查一长串数学推导的跳步是否合法。对于大模型生成的高层证明思路数学家可以用 Lean 把主要引理逐条形式化。4.3 为什么大模型无法替代证明器不严谨地说大模型是在做“模式联想”它擅长从训练语料里复现类似证明的结构但不保证每一步都符合逻辑规则。证明器则相反它不强求创新只要进入内核每个步骤都必须严格通过类型检查。把两者结合可以让大模型负责找到证明路径而证明器负责验证路径是否真的连通。5. 常见问题与排查链路实际跑这套流程时大概率会遇到下面这些问题。按“现象 - 原因 - 排查 - 解决”的顺序整理成表格方便直接对照。现象常见原因检查方式处理建议LLM 输出大量解释文字SymPy 解析失败提示词没有限制输出格式打印llm_output查看在提示词里写明“只输出一个表达式不要解释”或程序里做后处理表达式包含 LaTeX 命令sympify报错模型仍然使用了 LaTeX检查输出是否含\frac、\sqrt给模型示例输出要求使用Python风格或先写一个 LaTeX 解析层计算结果数学上相等但simplify 0返回 False表达式形式复杂SymPy 化简不彻底尝试sp.trigsimp,sp.expand,sp.apart使用sp.simplify后仍不通过再尝试多次变换或者手工检查关键项本地 Ollama 调用超时模型过大或首次加载慢查看 Ollama 日志CPU/GPU 占用换更小模型增加timeout提前做一次预热调用Lean 项目编译非常慢Mathlib 体积庞大观察编译日志第一次编译耐心等待不要在每次运行都重建使用lake env增量构建大模型对同一个问题多次回答不一致temperature 设置过高多跑几次看方差将 temperature 降到 0 或 0.1在业务层增加缓存符号计算内存爆满或卡死表达式太长或化简太激进观察 CPU 和内存先sp.expand替代sp.simplify限制表达式长度分段验证排查顺序建议先看模型输出原文再确认 SymPy 解析是否成功再看化简结果是否真的为零。大多数失败都在前两层不要一上来就怀疑证明器或数学理论。6. 从实验脚本走向生产级“世界思维”6.1 设计项目结构实验脚本可以随便写但生产环境需要把“调用模型”和“数学验证”解耦。推荐结构math-ai-workbench/ ├── config.yaml ├── main.py ├── llm_client.py ├── validator.py ├── lean_check/ # Lean 项目 │ ├── lakefile.lean │ └── Mathlib.lean ├── tests/ │ ├── test_validator.py │ └── cases.json └── requirements.txt6.2 配置外置化把模型名称、接口地址、温度、超时时间放到config.yamlllm: base_url: http://localhost:11434/v1 model: qwen2.5-math:7b temperature: 0.1 timeout: 120 validation: max_expr_len: 1000 simplify_timeout: 10 check_constant_equivalence: true加载配置时使用PyYAMLpip install pyyamlimport yaml with open(config.yaml, r, encodingutf-8) as f: config yaml.safe_load(f)这样切换本地模型、云端模型或内部网关时不需要改代码。6.3 增加日志和缓存在生产环境每一条“AI 生成 - 符号验证 - 证明器检查”的链路都应当留下记录。import logging import hashlib import json logger logging.getLogger(math_ai) logger.setLevel(logging.INFO) def make_cache_key(user_question: str, model: str) - str: payload json.dumps({q: user_question, m: model}, ensure_asciiFalse) return hashlib.sha256(payload.encode()).hexdigest()缓存可以用简单的 JSON 文件也可以使用 Redis。缓存的意义不只是省钱更是让同样的数学问题在相同模型配置下得到确定性结果便于回归测试。6.4 建立验证回归测试集把一组已知正确答案的题目放到cases.json中[ { question: sqrt(x**2 1) 的导数, func: sqrt(x**2 1), operation: diff, expected_kind: derivative }, { question: ∫ x*exp(x)*sin(x) dx, func: x*exp(x)*sin(x), operation: integrate, expected_kind: antiderivative } ]然后在tests/test_validator.py里写一个简单的回归测试import sympy as sp def test_derivative_cases(): x sp.Symbol(x) cases [ (sqrt(x**2 1), x / sp.sqrt(x**2 1)), (sin(x)*exp(x), sp.diff(sp.sin(x) * sp.exp(x), x)) ] for func_str, expected in cases: expr sp.sympify(func_str) actual sp.diff(expr, x) assert sp.simplify(actual - expected) 0这里不依赖 LLM只验证 SymPy 自身逻辑确保验证层本身不坏。再写一层 mock LLM 的测试模拟大模型输出验证主流程是否正确。6.5 学习环境与生产环境的差异维度学习环境生产环境模型本地小模型即可选数学微调模型或旗舰模型做评测选型验证SymPy 结果人工看一眼即可必须自动回归且引入 Lean/Coq超时默认 120 秒要分任务设置简单推导 30 秒复杂证明 10 分钟以上异常处理try except直接跳过必须有重试、降级、告警、人工复核通道安全本地运行没有密钥泄露风险密钥必须托管在密钥管理服务中可追溯只看最终输出保存 LLM 原始输出、模型版本、验证日志、证明文件版本6.6 实际项目中最重要的三条建议第一永远不要让大模型直接写最终证明结论。大模型适合生成草稿验证工作必须交给确定性的计算工具和证明器。第二不要急于把整个数学研究流程自动化。先把单个步骤的验证闭环跑通再扩展到多步推理最后再讨论“自主数学 Agent”。第三每一步的输入输出都要规范化尤其是数学表达式格式。LLM 输出自由文本程序只接受格式严格的表达式中间必须有清洗和解析层否则验证本身就会成为新的错误来源。现在这个最小工作流已经足以覆盖大模型生成求导或积分结果SymPy 进行符号验证Lean 对关键恒等式做形式化证明。在它之上进一步扩展可以加入多步推理任务拆分、数学 Agent 的记忆模块、多个模型投票、证明库自动搜索等功能。那个目标是“世界思维”但每一步都仍然要建立在可验证的工程基础之上。数学的“英雄时代”终结之后取而代之的不是某一个超级 AI而是一个由工具、数据和纪律构成的协作系统。