最近一年里越来越多的数学研究者和工程团队开始思考同一个问题大规模语言模型LLM除了能写代码、做问答还能不能真正推动数学前沿的发展我的判断是LLM 短期内不会像数学家那样独立写出惊世骇俗的证明但它已经在“生成猜想、补全证明片段、辅助形式化验证、加速审查过程”这四个环节里变成了一个不可忽略的加速器。真正值得投入的方向不是让模型单独给出“对的答案”而是把 LLM 当成假设生成器和形式化证明器的前端用 Lean、Coq、SymPy 这些确定性工具去校验它给出的每一条思路。这篇文章会把话题落在具体可操作的层面先说清楚 LLM 在数学发展中到底扮演什么角色再给出三套可以跑通的实践路径——自然语言证明草稿生成、Lean 形式化证明辅助、符号计算验证最后总结落地时最常踩的坑和工程化建议。无论你是做数学研究、做算法工程还是对 AI for Science 感兴趣都可以按这篇文章的思路搭出自己的最小验证环境。1. 这篇文章真正要解决的问题数学发展的最大瓶颈从来不是“算不出来”而是“不知道往哪个方向想”。传统计算工具擅长把已经形式化的命题验证清楚但不擅长在巨大搜索空间里生成“看起来有可能成立”的猜想也不擅长把一段自然语言思路转换成机器可检查的形式化证明。这两件事恰恰是 LLM 的长项也是当前 AI 辅助数学研究的价值所在。先说数学研究者会遇到的具体痛点。一是文献太多一个新定理可能依赖几十篇前序工作人工梳理等价条件和证明技巧非常耗时二是证明太长即使思路正确形式化到 Lean 或 Coq 里也常常要花数周时间三是猜想生成高度依赖直觉而直觉很难被自动化。传统符号计算系统可以验证恒等式、解方程但无法理解一个数学段落里的“语义”传统自动定理证明器虽然严谨但交互门槛高对自然语言输入几乎不友好。LLM 则补上了中间的缺口。它可以阅读论文摘要和证明片段生成一个候选证明的大纲可以把一段 LaTeX 描述转为 Lean 语法骨架可以为一个具体恒等式建议需要调用的库函数。但必须强调LLM 的输出不可信。它可能在第二步就引入一个错误的替换可能忽略一个前置条件也可能一本正经地构造一个不存在的引理。所以真正成熟的用法是把 LLM 当作“创造力的外挂”把形式化验证器当作“正确性的守门员”。因此本文的核心问题不是“AI 能不能做数学”而是“怎么让 LLM 在数学工作流里安全地加速”。我会重点回答三个子问题第一用哪些开源或 API 工具可以快速跑通一个数学辅助任务第二自然语言证明、形式化证明、符号校验这三条路径分别怎么落地第三哪些环节必须有人工把关哪些环节可以放心交给自动验证。2. 核心概念为什么 LLM 能参与数学发展但不能独立负责要理解 LLM 在数学发展中的作用先要区分三个层次的概念自然语言推理、形式化证明、符号计算。很多人把它们混为一谈实际它们在数学工作流里承担完全不同的职责。自然语言推理指的是 LLM 用人类可读的段落解释定理、给出证明思路。它最大的问题是没有确定性的正确性判断模型可能在一个看起来合理的推导里偷偷混入错误步骤。但在“给出候选想法”这个层面它的价值非常高因为数学研究的第一步往往是“想出一个有可能对的路径”而不是“证明一个确定对的结论”。形式化证明是把数学命题写进 Lean、Coq、Isabelle 这样的证明助手由机器逐步检查推理规则。这是目前最可靠的数学论证方式之一但代价是成本极高一个在论文里两三页的证明形式化到 Lean 里可能需要几百行代码。LLM 在这里的用武之地是“降低形式化门槛”——它可以帮人类把证明思路翻译成骨架代码再由人来修正和补全。符号计算则是用 SymPy、Mathematica 这类工具对表达式做精确的代数变换。它不依赖概率也不存在“幻觉”适合验证恒等式、化简表达式、检查特例。它和 LLM 的关系非常互补LLM 负责提出“这个式子可能恒等于另一个式子”SymPy 负责回答“到底等不等于”。从材料看目前主流的研究尝试都集中在“LLM 证明助手”的组合上。原因也很简单证明助手提供可验证的反馈信号模型生成的证明片段只有在通过编译和检查之后才算有效。这本质上是一个“生成-校验-修正”的循环。而在这个循环里LLM 是生成器校验器是确定性的修正环节由人或者由模型根据报错信息完成。这个闭环比单纯让模型生成文本要可靠得多。用一张简单的表来对比三种方式的定位方式代表工具正确性保障主要成本适合场景自然语言推理ChatGPT、开源 LLM无提示词设计与人工复核生成猜想、证明思路、论文阅读形式化证明Lean、Coq、Isabelle机器逐步验证写法复杂、编译反馈周期长把证明变成可检查代码符号计算SymPy、Mathematica确定性代数规则受限于算法能力化简恒等式、推导公式、验证特例我特别想纠正一个误区很多人以为“LLM 能做数学”等于“LLM 能输出正确答案”。实际在重大数学发展中模型输出的正确答案并不重要重要的是它能不能输出“值得人类去验证的候选答案”。数学的难度在于证明空间太大而 LLM 可以作为搜索策略的一部分缩小搜索范围。这才是在 AI for Math 里最有价值的定位。3. 环境准备本地推理、API 与证明助手的取舍要开始实践先准备好一套顺手的工具链。下面这些环境不是必须全部安装你可以根据自己手头的资源选择一条路径。我的建议是从本地小模型或 API 开始先跑通“生成思路 符号校验”最小闭环再考虑接入 Lean。Python 环境是基础建议使用 Python 3.10 或更高版本。核心依赖包括 transformers、torch、sympy 和 notebook。如果你使用 Hugging Face 的开源模型还需要留意 transformers 和 torch 的版本兼容性具体版本以你安装时的官方说明为准不要盲目追求最新版。Lean 环境的安装稍微特殊一点。Lean 4 配合 Mathlib 数学库是最常用的组合。它不像普通 Python 包那样直接pip install一般推荐使用 elan 来管理 Lean 的版本。安装完成后新建一个项目并添加 Mathlib 依赖然后执行lake exe cache get下载预编译缓存。这个过程依赖网络如果下载速度慢项目第一次编译会比较痛苦。如果走 API 路线需要准备一个可用的模型服务可以是 OpenAI 兼容接口也可以是国内大模型平台的 OpenAI 兼容端点还可以是本地部署的 vLLM 服务。无论选择哪一种最关键的是把 API 调用封装成统一函数方便后续切换模型。这里有一个容易踩坑的地方不同提供商对messages格式、max_tokens和temperature的命名可能略有差异调用前一定要看服务商文档。下面给出一个最小化的环境检查思路。你不需要一开始就搭完整的集群而是先用一个小脚本确认“模型能加载、SymPy 能计算、文件夹能保存中间结果”再逐步扩展。# 创建虚拟环境 python -m venv .venv source .venv/bin/activate # 安装核心依赖 pip install --upgrade pip pip install torch transformers sympy jupyter如果你只需要跑 Lean 部分则参考 Lean 官方文档安装 elan 和 lake然后新建项目elan self install lake new ai_math cd ai_math lake update lake exe cache get需要提醒的是这些命令只能代表通用流程具体版本和命令在不同环境下可能变化。从工程角度讲我更推荐先把 Python 侧的 Symbolic Check 跑通因为它的反馈最快错误最容易定位。等到你确认 LLM 的生成结果能被 SymPy 校验、能被你读懂再引入 Lean 提高形式化程度学习的性价比更高。4. 示例一用 LLM 生成数学证明草稿第一个示例解决一个很实际的问题给你一道数学命题如何快速获得一个可讨论的证明思路。这里选择“两个连续整数的平方差一定是奇数”作为演示题目。它足够简单但也足以展示 LLM 参与数学推理时容易出错的地方——它可能会默认n^2和(n1)^2的关系但忽略奇偶性的表达。在本地环境中我建议使用 Hugging Face 的pipeline接口加载一个支持指令的模型。这样可以省去手动处理 tokenizer 和 model 的细节。下面的代码以“Qwen 系模型”为例你也可以替换成其他模型名。注意模型名称和本地显存大小直接相关7B 模型通常需要 8GB 到 16GB 显存如果没有 GPU可以改用更小的模型或者走 API。# 文件路径examples/llm_proof_sketch.py from transformers import pipeline generator pipeline( text-generation, modelQwen/Qwen2.5-7B-Instruct, device_mapauto, ) system_prompt 你是一位严谨的数学助手只负责提供证明思路不要输出无关内容。 user_prompt ( 请给出一个证明思路两个连续整数的平方差一定是奇数。 不要直接写最终证明先说明关键的代数变形和奇偶性判断。 ) messages [ {role: system, content: system_prompt}, {role: user, content: user_prompt}, ] result generator( messages, max_new_tokens512, do_sampleTrue, temperature0.3, top_p0.9, ) print(result[0][generated_text][-1][content])这段代码的核心价值不在模型本身而在于它把“生成证明草稿”变成了一个可重复调用的函数。在真实工作流里你可以把user_prompt换成任意 LaTeX 命题把输出保存成 Markdown 文件再给下一环节的符号校验使用。运行这个脚本时需要注意几个细节。第一pipeline是否接受messages格式取决于你安装的 transformers 版本如果报错就退回到拼接字符串的普通方式。第二temperature不宜太高数学推理场景下取 0.2 到 0.4 更稳定如果目标是生成多个候选思路再适当调高。第三模型输出的文本往往带有“证明”“思路”这样的 Markdown 符号后续解析时要用正则表达式做清洗。从实际效果看LLM 对这个题目的典型输出是设较小整数为 n则另一个为 n1平方差为(n1)^2 - n^2 2n 1因此一定是奇数。这个思路是正确的但模型并不保证每次输出都正确。它会“忘记”解释 n 是整数或者把2n1写成2n-1却不检查定义域。这正好引出一个重要原则LLM 生成的草稿只是候选必须进入下一个验证环节。5. 示例二用 LLM 辅助 Lean 形式化证明如果说自然语言证明草稿是“给人看的”形式化证明就是“给机器看的”。Lean 4 是目前数学形式化领域最活跃的工具之一Mathlib 里已经积累了大量的数学定义和定理。把 LLM 接进来最常见的做法是让模型根据一个自然语言命题生成 Lean 代码骨架然后在 Lean 环境里编译根据编译错误反复修改。这个环节的体验很像程序员用 Copilot模型给出代码编译器说“这里有错误这个是 expected type那个是 actual type”你再把错误信息喂回给模型让它修改。如果一轮一轮迭代之后 Lean 依然报错往往说明模型对相关数学定义的理解确实有问题这时候人工介入是必要的。先看一个最简单的 Lean 4 示例。假设我们要证明自然数加法交换律。这个定理在 Mathlib 里已经存在但我们可以亲手验证一下模型是否能生成正确写法-- 文件路径MathTest.lean import Mathlib theorem add_comm_example (a b : Nat) : a b b a : by omega如果本地的 Lean 环境已经安装好 Mathlib这个文件应该能通过编译。omega是一个处理线性整数算术的策略它能自动证明这类初等的代数恒等式。如果你的 Lean 版本较老或者没有导入 Mathlib可能会提示unknown constant omega这时候改成库定理即可theorem add_comm_example (a b : Nat) : a b b a : Nat.add_comm a b这第二个写法直接引用了 Mathlib 里的既有定理可靠性更高但它的局限是只能证明已经被库覆盖的结论。如果你要证明一个全新命题就得靠策略手动推导。那么在真实工作流里LLM 到底怎么帮上忙举个例子。你有一个不熟悉的新定义想证明f (n1) f n 1这类简单命题。你可以把定义代码和命题一起丢给模型让它生成一个战术块-- 这段代码由 LLM 生成仅作演示需要人工检查 theorem example_seq (n : Nat) : n 1 1 n : by omega把这段代码放进 Lean 文件里编译如果通过说明模型生成的策略确实起到了作用如果失败复制报错信息回到模型上下文继续追问修改建议。这个“编译错误反馈循环”比单纯让模型自由发挥要高效得多因为它给模型提供了一个明确的失败信号。不过要提醒一个关键点Lean 的编译错误信息对新手并不友好。常见错误包括unknown identifier、type mismatch、unsolved goals。遇到这些错误时不要急着改代码先看错误信息指向哪一行再判断是变量名错了、类型不匹配还是缺少前置条件。在这个循环里LLM 最大的价值不是一次性写出完美代码而是快速提供一个可迭代的起点。6. 示例三LLM SymPy 做符号计算验证形式化证明的代价高自然语言证明的可靠性低符号计算则站在中间它不需要你写完整的证明项但仍然能确定性验证一类代数恒等式。对于很多数学猜想的初筛SymPy 是性价比最高的工具。继续用“两个连续整数的平方差是奇数”这个命题。我们让 LLM 生成一个候选等式然后用 SymPy 检查左右两边是否真的相等。如果相等再看奇偶性如果不相等直接淘汰这条候选思路。这里的关键是把“数学直觉”和“代数正确性”解耦。# 文件路径examples/sympy_verify.py import sympy as sp n sp.symbols(n, integerTrue) left (n 1)**2 - n**2 right 2*n 1 difference sp.simplify(left - right) print(left - right , difference) if difference 0: print(恒等式成立平方差可以化简为 2n 1) print(奇偶性判断2n 1 恒为奇数) else: print(恒等式不成立候选思路应该被淘汰)运行这段代码预期输出是left - right 0随后打印“恒等式成立”。这个验证过程是确定性的只要 SymPy 的算法正确结果就可以信赖。你可能觉得这个例子太简单。那就把它扩成一个更接近真实研究的场景一个模型提出“某类特殊矩阵的特征值之和等于矩阵的迹”你可以随机生成几十个具体矩阵用 SymPy 逐一验证而不是直接证明一般情况。这种“随机实例检验”虽然不能代替证明但能快速淘汰明显错误的猜想。在机器学习的数学发现研究中这也是常用的筛选手段。可以用下面的代码做一个随机矩阵的快速验证import random import sympy as sp def random_matrix(rows, cols): return sp.Matrix([[random.randint(-5, 5) for _ in range(cols)] for __ in range(rows)]) for _ in range(20): A random_matrix(3, 3) lhs sum(A.eigenvals().values()) rhs A.trace() if sp.simplify(lhs - rhs) ! 0: print(发现反例猜想不成立) break else: print(20 组随机实例中候选关系均成立)注意Matrix.eigenvals()返回的是特征值到重数的字典所以sum(A.eigenvals().values())是所有特征值的代数和。这样写能快速验证一个线性代数猜想在随机实例上的表现。虽然它不能证明一般情况但能给你一个“值得继续投入”的信号。把三个示例串起来看就形成了一条完整的流水线LLM 生成候选思路SymPy 或随机实例做初筛Lean 做严格形式化证明。每一步的代价递增但可靠性和确定性也递增。实际项目中你应该根据命题难度和预期收益决定在哪一层停止。不是所有猜想都值得形式化到 Lean很多研究假设只需要符号验证就足够了。7. 运行结果与效果验证思路运行完上述示例后怎么判断自己的工作流是否真正有效我认为要回答三个问题生成是否稳定、校验是否明确、迭代是否收敛。第一个问题是生成是否稳定。同样一个命题LLM 跑五次可能给出五个不同结果。在数学场景下稳定性很重要如果五个结果里有两个是错的那就说明模型对这个领域的理解不够可靠不能直接用于批量任务。你可以在代码里对同一 prompt 做多次采样然后统计正确率。这个方法非常直观只有统计意义上达到你想要的比例才适合把生成环节接入自动化流程。第二个问题是校验是否明确。SymPy 给的0和 Lean 给的Goals accomplished是明确信号自然语言讨论则可能充满模糊。如果你的验证环节只能得到“看起来差不多”“应该是对的吧”那这条流水线还需要继续改造要么把结果转成更严格的表达式要么让模型输出更适合机器检查的结构化数据。第三个问题是迭代是否收敛。在 Lean 场景中你通常会经历“生成-编译-报错-修改-再编译”的多轮循环。一个高效的数学辅助系统应该让这个循环轮次越来越少。我的建议是在提示词里明确要求模型输出“只包含 Lean 代码”的格式把错误信息完整贴回上下文并指出代码行号。当模型连续三次修改仍然无法编译时就不要再绕圈子直接人工介入。为了验证整体效果你可以准备一个包含 5 到 10 个命题的小数据集每个命题的难度从“一行simp能证明”到“需要ring或omega”逐步递进。然后记录每次测试的生成是否成功、编译是否通过、人工修正需要几分钟。这份记录比任何感官评价都更能说明问题。8. 常见问题与排查思路实践过程中我整理了最常遇到的几个问题。这些问题不是某一个模型特有的而是把 LLM 和数学工具链结合时普遍会碰到的。问题现象可能原因排查方式解决方案模型输出包含大量“证明”“思路”等噪声文本提示词没有限定输出格式打印原始输出检查模板中的分隔符在 prompt 中明确“只输出 Lean 代码块”或“只输出数学表达式”SymPy 恒等式判断失败但人工看是正确的符号定义缺少整数或有理数假设打印中间表达式的假设集合用positiveTrue、integerTrue等约束重新声明符号Lean 报unknown identifierMathlib 未下载或导入缺失查看错误信息中的名字确认是否在 Mathlib 范围先执行lake exe cache get再确认import Mathlib在文件顶部本地模型推理速度慢模型过大或未使用 GPU查看 PyTorch 是否识别 CUDA调整device_mapauto或换更小的模型或走 APIAPI 调用偶尔超时服务端负载高或网络不稳定记录失败时间点和错误码增加重试机制和请求间隔把长 prompt 拆小多次生成结果差异大采样参数设置不合理检查 temperature 和 top_p数学任务建议 temperature 调到 0.2 以下或直接用do_sampleFalseLean 证明目标太大模型频繁失败不适合一次生成完整证明把命题拆成若干中间引理人先写引理结构模型只负责补全每个引理内部步骤这里最核心的建议是不要追求“LLM 一次性给出完整且正确的证明”。真实工作流中LLM 更像是“引理生成器”负责把大证明切分成多个小目标或者为某个卡住的目标提供备选策略。一旦你强迫模型一次性处理过大的证明目标错误率会急剧上升。另外不同 LLM 对数学符号的敏感度差异很大。有些模型在处理复杂 LaTeX 时会把\sum_{i1}^n理解成普通文本导致后续步骤完全偏离方向。因此在把命题输入给模型之前最好先用简单规则把 LaTeX 转成更结构化的描述或者要求模型保持原始 LaTeX 不变避免二次解析误差。9. 最佳实践与工程建议如果要把这套方法真正用进日常研究或工程下面几个建议值得记住。第一隔离生成与验证。不要让 LLM 既生成答案又自我检查。在代码结构上生成模块和验证模块必须分开验证模块只能由确定性工具承担。哪怕是简单的 SymPy 恒等式检查也比模型“我觉得正确”可靠得多。这个原则适用于所有 AI for Science 场景。第二记录中间过程。每一次模型生成、每一次验证结果、每一次 Lean 编译错误都应该以文本文件形式保存下来。这样你才能复盘模型在哪个环节开始出错也方便批量测试不同策略的效果。用 JSONL 保存三元组输入命题、模型输出、验证结果是成本最低的做法。第三提示词要工程化。数学类提示词不能太随意。我的通用模板是先定义角色再给任务背景然后限制输出格式最后给出示例。一条好的提示词应该让模型明确知道“输入是什么、输出要达到什么格式、正确性由谁负责”。对 Lean 任务还应该在提示词里强调“只输出可编译的 Lean 代码不要解释”或给出一个最短可编译片段作为样例。第四从小定理开始。不要试图让 LLM 直接参与黎曼猜想这类问题。建议从 Mathlib 里的简单引理入手先跑通“生成-编译-修正”循环再逐步提高命题难度。这个积累过程会帮助你评估模型的能力边界也能让你更熟练地读懂 Lean 的报错信息。第五重视“反例生成”。LLM 不仅可以用在正向证明也可以用来生成反例。当你想证明一个命题但总是卡住时试着让模型构造一个“可能破坏命题的反例”再用符号计算或随机实例去验证这个反例是否成立。如果反例成立说明原命题确实有问题你就省下了大量时间。这种“反向搜索”往往是数学研究里最容易被忽略的高杠杆操作。第六保持合理的预期。当前 LLM 参与的数学工作绝大多数还停留在“辅助”阶段。它可以帮你快速定位一个恒等式可以帮你生成形式化代码的骨架但还不足以独立完成一篇有开创性意义的数学论文。判断一个工具是否适合你标准不是它“有没有智能化”而是它能否稳定地把你的研发时间缩短哪怕 20%。10. 总结与下一步实践方向这篇文章真正想表达的核心观点其实很简单LLM 在重大数学发展中的价值不在于替代数学家而在于把“从思路到可验证证明”这条链条上的摩擦成本降下来。自然语言生成负责提供候选思路SymPy 和随机实例负责快速淘汰错误方向Lean 负责把最终结论变成机器可检查的形式化证明。三者结合才是一条值得长期投入的技术路线。你可以从最小的闭环开始实践准备一个 Python 环境装好 transformers 和 sympy写一个脚本让 LLM 生成一个简单恒等式的证明思路再用 SymPy 验证。跑通之后再逐步加入 Lean 环境尝试让模型生成一条简单定理的形式化代码。不要一开始就投入大量资源去训练自己的数学专用模型先用现成的开源模型和 API 把工作流验证清楚后续需要再针对特定领域做微调。近期值得继续关注的方向包括大模型在交互式定理证明中的战术生成、数学语料驱动的领域微调以及 Lean 和 LLM 之间的双向反馈机制。最后一个提醒任何 AI 生成的结果在正式写进论文或项目之前都必须经过人可以理解的验证步骤。数学是一个不允许模糊的领域越是强大的生成工具越需要同样强大的校验机制来兜底。