在近两年的数学研究和教学工作中AI 尤其是 LLM 的角色已经从“能聊数学问题”逐步变成“能参与数学发展流程的辅助工具”。所谓重要数学进展major mathematical developments并不只指证明某个公开猜想也包括构造反例、整理证明思路、把自然语言证明形式化、为数值实验设计计算方案等工作。LLM 的用途集中在这些流程中“生成候选、解释思路、转换表达、辅助验证”的环节而最后的正确性判断仍然需要人的推理和机器验证共同完成。这篇文章会带你搭建一套可以实际运行的 LLM 数学辅助工作流包含环境配置、最小示例、提示词策略、验证方法和常见坑排查。1. 先想清楚LLM 在数学发展中到底承担什么角色1.1 数学研究链条里哪些环节能交给 LLM数学研究并不是只有“证明定理”这一个动作。一个完整的数学进展通常包含提出问题、寻找候选结论、设计证明思路、完成符号推导、编写数值实验、形式化验证、审阅和返工等多个环节。不同环节的容错率完全不同LLM 能承担的角色也完全不同。下表是一个比较实用的分工视图数学工作环节LLM 可参与程度需要的配套工具典型产出文献调研与知识问答高检索接口、PDF 解析、向量库概念地图、文献摘要、历史脉络猜想生成中数值计算库、序列分析工具候选公式、可验证命题证明思路设计中低形式化证明助手证明骨架、引理拆分符号推导低LLM 负责表达计算器负责计算SymPy、SageMath、Mathematica可执行推导代码形式化证明中Lean、Coq、Isabelle可编译定理审稿与找错中调试器、定理证明器反例或错误定位这个表想说明一个核心判断LLM 不是用来替代数学家的判断力而是用来降低“从想法到可验证表达”的转换成本。真正负责把关的应该是符号计算器、定理证明器和人的审查。1.2 LLM 的数学推理边界它是启发式生成器不是裁判很多新手会犯同一个错误把 LLM 当作数学权威问完就抄结果。理解边界要从模型原理说起。LLM 本质上是在学习大量文本之后根据上下文逐词预测最合适的下一个 token。它优化的是“看起来像正确数学文本”的概率而不是“在逻辑上为真”的概率。因此 LLM 给出的任何数学结论都必须经过外部校验。即使它给出的证明步骤在局部看起来无懈可击也可能在某个隐含假设上出错即使它的语气非常自信也可能把两个不同定理的条件混在一起。正确的用法是把 LLM 当成“生成器”把验证器当成“裁判”。生成器负责提供候选裁判负责判决人负责设计验证策略和最终决策。注意当你要求 LLM 证明一个定理时第一反应不应该是“它说的对不对”而应该是“它给出的断言能不能转成一个可执行的检查”。2. 搭建一套能跑通数学辅助流程的环境2.1 模型选择与访问方式选择模型时不需要一上来就追求最大参数版本而是看数学推理和代码生成能力是否够用。常见做法分两条路线在线 API 路线调用当前可用的商用模型接口优点是部署成本低、数学能力较强缺点是数据隐私和费用需要评估。具体用哪家、什么版本要以你实际申请到的接口为准。本地模型路线使用 Ollama 或 vLLM 加载开源数学系模型例如 Qwen2.5-Math、DeepSeek-R1 等。优点是数据可控、可离线实验缺点是显存要求高推理速度不如在线接口。两条路线可以抽象成同一个函数调用给一个 prompt返回一段文本。这样做的最大好处是后续所有示例代码都可以在同一套接口上运行不需要因为换模型而重写逻辑。场景推荐方式注意点快速原型验证在线 API注意 token 限制和输出稳定性隐私数据或离线环境本地模型确认显存、量化精度和数学能力自动化批处理本地模型设定超时、重试和结构化输出学习调试在线 API 或本地均可用温度低参数减少随机性2.2 创建 Python 项目和依赖下面用一个最小项目math-llm-lab作为实验环境。这个项目会把 LLM 调用、符号计算、验证逻辑放在同一套代码里方便连成管线。mkdir math-llm-lab cd math-llm-lab python -m venv .venv source .venv/bin/activate pip install -r requirements.txt在项目根目录创建requirements.txtrequests2.32.3 openai1.48.0 sympy1.13.2 python-dotenv1.0.1 jupyter1.0.0解释一下为什么选这些依赖openai是调用 OpenAI 兼容接口的客户端sympy用于符号验证python-dotenv用于读取 API Key避免把密钥写进代码jupyter用来做交互式探索方便一格格观察输出。2.3 把 LLM 和符号计算器连成一条管线数学辅助工作流不建议“问一句答一句”而是建议设计成管线输入数学问题LLM 生成候选表达式或证明步骤解析器提取结构化内容符号计算器或定理证明器验证最后把验证结果返回给人。下面这段代码演示了一个最小封装把 LLM 调用和 SymPy 验证放在一起import os import openai from sympy import sympify, simplify client openai.OpenAI( base_urlos.getenv(LLM_BASE_URL, https://api.openai.com/v1), api_keyos.getenv(LLM_API_KEY), ) def ask_expression(problem: str) - str: resp client.chat.completions.create( modelos.getenv(LLM_MODEL, gpt-4o-mini), messages[ {role: system, content: 你只输出 LaTeX 数学表达式不要解释。}, {role: user, content: problem}, ], temperature0.2, ) return resp.choices[0].message.content.strip() def verify_identity(candidate: str, x_sym) - bool: expr sympify(candidate) return simplify(expr) 0这里的关键点是ask_expression负责生成verify_identity负责判断。不要把 LLM 的文本输出直接当作结论而是先转成 SymPy 表达式再验证。实际项目中base_url、api_key、model都应该从环境变量读取禁止硬编码。3. 三个最小可运行示例从“聊天”变成“开发”这一节通过三个示例说明 LLM 在数学发展中三种典型用法触发猜想、把自然语言推导转成可执行计算、生成形式化证明骨架。三个示例都遵循同一个原则LLM 只做生成验证交给机器。3.1 示例一用数值实验触发猜想很多数学猜想最初来自数值观察但观察数据本身往往稀疏、无序。LLM 可以帮助从数据中提出候选公式。比如先给模型一组序列数据请它猜测规律。import openai import os client openai.OpenAI( base_urlos.getenv(LLM_BASE_URL, https://api.openai.com/v1), api_keyos.getenv(LLM_API_KEY), ) data { 1: 1, 2: 4, 3: 9, 4: 16, 5: 25, 6: 36, } prompt f 我做了数值实验得到 n 与 f(n) 的对应关系 {data} 请给出一个最自然的候选公式用 LaTeX 表示。 只输出公式不要输出解释。 resp client.chat.completions.create( modelos.getenv(LLM_MODEL, gpt-4o-mini), messages[{role: user, content: prompt}], temperature0.2, ) print(resp.choices[0].message.content)如果模型输出f(n) n^2这只是候选。接下来要做的不是停止而是用更多数值验证并继续追问“为什么”for n in range(1, 100): if n * n ! sum(2 * k - 1 for k in range(1, n 1)): print(候选公式与数值实验结果不一致) break else: print(前 99 项数值验证通过)这段代码验证的是前 n 个奇数的和等于 n 的平方。一旦候选公式通过数值验证才能进入下一步思考它是否由已知定理推导得出。这里有一个重要提醒数值通过永远不等于证明。它可以提高置信度也可以暴露错误但唯一能作为最终结论的是完整逻辑证明或形式化验证。3.2 示例二把自然语言证明步骤转成 SymPy 验证数学推导中最容易被 LLM“一本正经地编错”的场景是恒等式化简。比如让 LLM 判断一个三角函数恒等式是否成立它可能直接给出“成立”但实际缺少条件。更稳妥的方式是让 LLM 生成一个候选表达式然后用 SymPy 去验证。from sympy import symbols, simplify, sin, cos, tan, expand x symbols(x, realTrue) # 候选恒等式sin(x)^2 cos(x)^2 1 candidate sin(x) ** 2 cos(x) ** 2 - 1 print(化简结果:, simplify(candidate))预期输出是0代表该恒等式对实数 x 恒成立。如果把候选改成(sin(x) cos(x))^2 1化简结果不会为 0说明它不成立。这个例子的工程含义是LLM 可以负责把“人类语言的推导”转换成数学表达式但转换结果必须能在符号环境中执行。SymPy 的simplify、expand、factor、equals都是常用的校验函数。注意SymPy 的sympify只能解析它支持的语法LLM 输出的 LaTeX 需要先用parse_latex之类的工具转换或者让模型输出 Python/SymPy 语法而不是 LaTeX。3.3 示例三LLM 生成 Lean 4 证明骨架再由编译器把关形式化证明是数学发展的另一个重要方向。Lean 4 是目前社区活跃度很高的证明助手。LLM 在这里的用法不是直接证明所有定理而是生成证明骨架和中间目标再由 Lean 的编译器检查每一步是否合法。先用 elan 安装 Lean 4 工具链并在 VS Code 中安装 Lean 插件curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash mkdir -p math-llm-lab/Lean cd math-llm-lab/Lean创建一个最简单的验证文件Test.leanimport Mathlib.Data.Real.Basic example (a b : ℝ) (h : a b) : a ^ 2 b ^ 2 : by rw [h]这是一个非常基础的示例如果 a 等于 b那么 a 的平方等于 b 的平方。LLM 可以学习这类证明模式然后在一个大定理的背景下生成若干中间步骤但每个步骤必须通过 Lean 的类型检查。遇到不通过的步骤就把 Lean 的错误信息回传给 LLM让它重新生成形成“生成—检查—反馈—再生成”的循环。注意Lean 的版本、Mathlib 版本不一致会导致大量无意义报错。项目里建议固定版本并把版本信息写在 README 或 CI 配置里。4. 让数学任务稳定输出的提示词设计与参数选择4.1 生成参数温度不是越高越好LLM 的采样参数对数学输出影响很大。数学推理需要确定性而发散性任务需要多样性。参数常见范围数学证明与化简猜想搜索与头脑风暴temperature0 到 20 到 0.30.7 到 1.0top_p0 到 10.1 到 0.50.8 到 0.95max_tokens视模型而定足够容纳完整推导允许较长的逐项分析stop自定义遇到分隔符停止用于结构化输出结束从实践角度做数学验证类任务时推荐先把 temperature 设为 0避免模型在同样的 prompt 下输出不同结果。只有在探索猜想、生成反例候选时才提高温度让模型给出更多样化的假设。4.2 数学提示词模板面向数学任务的 prompt 与普通提问不同。普通提问容易得到“综合回答”数学任务最好要求模型输出结构化、可检查的内容。下面是一个可复用模板你是一名严谨的数学研究助手。当你处理数学问题时必须遵守以下规则 1. 先用一两句话复述问题确保理解正确。 2. 把证明或推导拆成编号步骤每步注明使用的前提条件。 3. 涉及恒等式化简时输出一个可被 SymPy 解析的表达式。 4. 如果存在边界条件或反例显式写出。 5. 结论必须放在 结论 之后便于程序解析。 问题这里放你的数学问题添加“复述问题”这一步可以显著降低模型答非所问的概率。因为模型在生成回答前先被迫把问题语义压缩成自己的表述如果理解偏差人马上能看出来。4.3 把对话式交互改成函数式调用在科研流程中更推荐函数式调用而不是交互式聊天。原因是函数调用可以方便地做批处理、缓存和日志记录。比如把所有数学提问统一封装成ask_math_tasks返回 JSON方便后续自动验证。import json def ask_math_tasks(problem: str) - dict: prompt f 你是数学助手。请按 JSON 格式回答字段包括 - restatement: 问题复述 - steps: 推导步骤列表 - conclusion: 最终结论 问题{problem} resp client.chat.completions.create( modelos.getenv(LLM_MODEL), messages[{role: user, content: prompt}], temperature0.2, response_format{type: json_object}, ) return json.loads(resp.choices[0].message.content)这种做法的好处是输出的 JSON 可以直接进入下一步验证管线而不用靠正则从自然语言中抽取内容。注意response_format参数并不是所有模型都支持本地模型可能需要改用“只输出 JSON不要输出其他文本”的提示词。5. 输出的数学结果必须经过三层验证才能进入研究流程5.1 数值抽查用随机数据暴露错误数值验证是成本最低的第一层防线。无论是恒等式、不等式还是近似公式都可以用随机采样验证。下面代码检查一个 LLM 给出的恒等式是否在大量随机点上成立import random from math import sin, cos count 10000 for _ in range(count): x random.uniform(-1000, 1000) lhs sin(x) ** 2 cos(x) ** 2 rhs 1.0 if abs(lhs - rhs) 1e-9: print(发现反例:, x) break else: print(f{count} 个随机样本均通过)注意随机点可能落在函数的奇点附近也可能因为浮点误差出现误报。所以数值抽查适合“快速排除明显错误”不适合给出正确性终审。遇到在特殊点不成立的候选公式多半是因为模型遗漏了定义域条件。5.2 符号验证SymPy 做精确化简数值验证通过后进入符号验证。好处是可以在不做近似的情况下判断表达式是否恒等。以 SymPy 为例from sympy import symbols, simplify x symbols(x) # LLM 给出的恒等式 lhs (x 1) * (x - 1) rhs x ** 2 - 1 print(simplify(lhs - rhs)) # 0 表示恒等SymPy 的simplify并不总能对复杂表达式给出最简形式所以如果一个恒等式验证失败先不要急着否定可以尝试expand(lhs - rhs)、factor(lhs - rhs)或者使用trigsimp、powsimp等专用化简函数。这也是工程上的常见坑验证器本身的能力边界会影响判断结果。5.3 形式化验证Lean 4 把证明交给类型检查器对于需要作为研究成果的定理最终推荐落到形式化证明工具。Lean 4 把数学证明变成了一组可以被编译器检查的命令。import Mathlib.Data.Real.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric example (x : ℝ) : sin x ^ 2 cos x ^ 2 1 : by exact ?_在最开始写exact ?_只是为了先让 Lean 显示当前目标再根据目标逐步补充证明。LLM 可以在这个阶段生成候选 tactic 序列但每个 tactic 都必须通过 Lean 检查。实际上这里推荐把 LLM 当作用来生成“下一步要做什么”的辅助而不是期望它一次性输出完整证明。三种验证方式的定位如下表验证层工具示例计算性质结论强度适用场景数值抽查Python random浮点近似仅排除明显错误快速筛选候选符号验证SymPy、SageMath精确符号运算可判断恒等式论文推导、公式化简形式化验证Lean、Coq、Isabelle逻辑证明检查证明完全可靠正式成果、大型定理5.4 最后检查 LaTeX 可编译数学论文里LLM 输出的 LaTeX 经常存在无法编译的问题常见的包括\left...\right不配对、自定义宏未定义、缺少%转义。处理方式是让模型输出“只含公式”的内容然后用pylatexenc或临时 LaTeX 文档检查可编译性。pip install pylatexencfrom pylatexenc.latex2text import LatexNodes2Text latex r\sum_{k1}^{n} k \frac{n(n1)}{2} text LatexNodes2Text().latex_to_text(latex) print(text)这一步虽然不校验数学正确性却能避免把“无法编译的公式”带进论文草稿。实际项目中可以把 LaTeX 检查放在 CI 里每次修改论文源文件后自动跑一遍。6. 常见坑与排查路径6.1 五个高频问题问题现象可能原因检查方式处理建议模型自信地给出错误恒等式LLM 生成的是近似正确文本不是逻辑判断随机抽样数值验证、SymPy simplify所有结论强制走验证管线不直接采信输出的 LaTeX 无法编译定义了不存在的宏、括号不配对pylatexenc 或 LaTeX 文档编译要求模型只输出公式在 CI 中加入编译检查浮点数验证整数结论数据溢出或浮点误差更换为大整数、Fraction、有理数类型整数类结论用整数运算或形式化证明验证Lean 代码大量报错Lean 或 Mathlib 版本不一致查看lake env lean版本和报错信息固定版本统一用 elan 工具链同样 prompt 每次结果不同temperature 设置过高打印采样参数和完整 prompt验证类任务 temperature 设为 0并记录 seed6.2 排查一条生成结果的完整路径当发现 LLM 输出结果异常时按下面的顺序排查能快速定位问题在哪个环节先确认输入问题本身是否表达完整。问题含糊、缺少定义域和条件模型自然容易答偏。再确认 prompt 是否要求结构化输出。如果没有结果可能被解释性文本污染。检查模型参数。temperature、top_p 是否在验证场景下过高。检查解析环节。SymPy 解析失败时优先看 LaTeX 中是否有 SymPy 不支持的语法。检查验证器本身。SymPy 对某些特殊函数化简不彻底不代表命题必然错误。检查版本。Lean、Mathlib、SymPy 的版本差异会改变可用的 API 和化简行为。最后回到数学判断。如果所有机器验证都通过再询问自己这个结论是否合理是否遗漏了边界条件。顺序遵循“输入 - 生成 - 解析 - 验证 - 版本 - 数学判断”的原则每一步都能通过打印日志和中间结果确认。7. 从实验到研究可复用的工作清单与下一步方向7.1 使用 LLM 做数学辅助的检查清单下面这份清单适合在每次把 LLM 输出引入研究流程前逐项核对问题是否明确到“可判定”是否存在反例空间、定义域是否完整。prompt 是否限制了输出格式JSON、LaTeX 或 Lean 代码要明确指定。是否关闭了随机性验证类任务 temperature 是否设为 0。是否做过数值抽查至少覆盖正常区间和边界点。是否做过符号验证能用 SymPy 化简的恒等式不能只靠肉眼判断。是否做过形式化验证正式成果是否进入 Lean 或 Coq 检查。是否保留完整日志prompt、输出、验证结果、版本号是否可回放。是否由人做了最终判断模型结论在整体证明策略中是否合理。7.2 学习环境与研究环境的差异维度学习实验环境正式研究/生产环境数据隐私可直接调用在线 API需评估隐私必要时本地模型验证强度数值抽查即可需要符号验证加形式化证明日志打印在 Jupyter 即可落盘、版本化、可追溯API Key 管理环境变量密钥管理服务错误处理直接报错就行超时、重试、失败降级版本控制可有可无Lean/Mathlib/SymPy 版本全部固定7.3 可以继续深入的方向数学论文知识库把已发表的论文解析后存入向量数据库用 RAG 让 LLM 在回答前先检索相关定理和上下文减少幻觉。定理证明智能体构建“LLM 生成步骤 Lean 检查 错误回传”的循环逐步提高自动化证明的长度和复杂度。多智能体协作一个模型负责猜测引理另一个模型负责找反例第三个负责形式化形成互相验证的闭环。从教学到科研的迁移先在课堂和练习题中跑通流程再逐步用于文献整理、公式纠错和论文草稿检查。实际做项目时最值得优先投入的是验证管线而不是模型本身。模型总会迭代API 总会变但“任何生成结果都必须经过外部验证”这一原则是长期有效的。把这条原则固化到代码里LLM 才能真正成为数学发展中可靠的生产力工具。