最近两三年数学界与人工智能社区的交叉比以往任何时候都要密集Lean 证明助手被用来推进顶尖分析学结论的形式化验证深度强化学习模型在几何问题上给出了人类选手级别的解答“自动形式化”这一概念也开始从论文走进工程实践。本文想从技术角度聊一个更大的话题当 AI 真正参与数学的发现、证明与传播时延续了几百年的“英雄时代”是否正在落幕数学家的工作方式又会从“个体天才驱动”走向怎样的新范式1. 背景数学的“英雄时代”是什么1.1 数学史中长期存在的“天才叙事”翻开数学史我们会看到大量以“天才个体”为核心的故事欧拉凭一己之力建立分析学的基础伽罗瓦在决斗前夜写下群论思想黎曼用一篇短短的论文改变了整个几何学方向拉马努金一边靠直觉写下公式一边等待后人验证格罗滕迪克几乎凭个人努力重构了代数几何的框架。这种“英雄时代”并不仅仅是一种叙事风格它背后有一套完整的研究方法论某个数学问题被英雄式的人物提出又由同一个人凭直觉找到解法最后由小圈子的同行在论文和学术通信中完成验证。整个过程高度依赖单个大脑的工作记忆、短期注意力和灵感爆发数学也因此被看作最需要“天才”的学科。从技术角度来看这样的研究方式并非人类天生就适合而是受限于纸质传播和人工推导的客观条件在必须靠纸笔验证的时代个体洞察确实是最高效的生产力来源。但代价也很明显证明过程难复现、错误难以发现、知识高度中心化。1.2 为什么说“英雄时代”正在结束进入 20 世纪后半叶数学研究对象越来越复杂单个证明动辄上百页。最典型的例子是有限单群分类定理它的证明分散在数百篇论文中总篇幅超过一万页至今仍有数学家认为“完整验证”本身就是一个难以完成的工程。计算机的出现改变了这一切。四色定理在 1976 年首次通过计算机辅助证明随后 Kepler 猜想也在 1998 年被机器辅助验证。这类工作标志着一个转折数学证明的正确性不再由某个天才大脑完全把控而是转移给了“可枚举的计算过程”。当 Lean、Coq、Isabelle 等交互式证明助手进入主流视野后数学验证的颗粒度又进一步下降每个符号、每条推理规则都能由机器检查。近年 AI 技术的冲击则更直接。符号计算系统让代数变形变成自动化的查表操作深度学习模型能在大量数学数据中搜索模式强化学习模型在平面几何、数论实验等任务上开始做出接近人类选手的判断。数学家已经不能忽视一个事实机器不仅在“帮我们算”还在“替我们想”。1.3 何谓“世界心智”“World-Mind”并不是科幻意义上的单体超级智能而是一种去中心化的认知网络人类研究者负责提出方向、构造抽象概念机器负责大规模搜索、符号演算、形式化验证群体则通过开源社区、形式化证明库和可复现代码共同维护知识的正确性。在这种新范式下数学的发现不再是一个大脑在封闭空间里的顿悟而是多个大脑与多台机器组成的协作系统共同完成的过程。单个数学家仍然重要但其重要性的来源不再是“一个人能战胜所有支线”而是“这个人能提出值得机器去验证的问题”。2. 当 AI 走进数学主要技术路线2.1 定理证明器从 Coq 到 Lean定理证明器是“英雄时代”终结最直接的工程标志。它把数学证明变成一种可执行的程序我们写出定理声明然后用一系列推理规则构造证明项最后交给内核检查。检查过程是机械的、确定的不存在“我认为这个引理显然成立”的模糊空间。Lean 是目前社区热度较高的一套证明助手。它的一大特点是数学库 Mathlib 组织得非常好覆盖了大量基础数学内容。一个广为人知的标志性事件是 Liquid Tensor ExperimentPeter Scholze 提出了一个分析学中的关键猜想Lean 社区通过形式化工作把它翻译成机器可验证的证明进而帮助数学家确认了其中一些此前悬而未决的技术细节。从工程视角看定理证明器的价值不是取代数学家的思考而是把“审稿人靠直觉判断”转变成“机器靠规则判断”。一个证明只要通过内核检查它就不再需要被同行反复阅读每一个符号因为它已经被压缩成了一段可复现、可审计的代码。2.2 自动形式化把论文变成代码自动形式化Autoformalization是连接自然语言数学与定理证明器的桥梁。数学家习惯用自然语言写“我们考虑一个连续函数 f”而定理证明器要求我们精确地表达“f 的类型是什么、定义域是什么、连续性是在哪个拓扑意义上定义的”。这个转换通常非常繁琐也是很多人刚接触证明助手时最大的挫败来源。近几年大语言模型开始被用于辅助这一过程模型阅读一段论文陈述尝试生成对应的 Lean 或 Coq 代码再由证明器判断代码是否正确。这种“生成-验证”循环对幻觉有天然约束因为即使模型胡编了一个定理证明器也会立刻报错。需要注意的是自动形式化目前远未成熟。对于复数乘法、测度论积分这类高度重构的数学对象自然语言到形式语言的翻译仍然需要人工介入。它的工程意义在于降低了新用户的上手门槛让数学家可以更多聚焦在问题本身而不是证明系统语法。2.3 符号计算与猜想发现符号计算系统是 AI 数学研究中常常被低估的一环。SymPy、SageMath、Mathematica 擅长处理多项式展开、因式分解、微分、积分、方程求解等操作。严格来说它们不是“思考”但在实验数学中它们是发现猜想的发动机。典型的做法是当一个数学家怀疑某个恒等式成立时先用符号计算生成大量特殊取值快速验证前一百项、前一千项再决定是否值得投入时间做证明。这种“机器实验 人类证明”的组合已经持续了几十年AI 的作用在于把原来依赖手工的试错变成自动化的统计搜索并能覆盖更高维、更复杂的对象。2.4 强化学习与搜索AlphaProof 思路的启示AlphaProof、AlphaGeometry 这类系统采用的方法是把数学问题视为一个搜索问题通过强化学习不断生成证明步骤再用符号引擎或证明助手判断每一步是否合法。这种思路和证明助手的“校验”角色天然互补校验器负责判定对错搜索器负责寻找路径。在奥数几何题这种规则空间相对封闭的任务上这种组合已经能接近人类选手水平。背后的工程实现并不神秘一个策略网络负责生成候选步骤一个价值网络负责评估“大概率有前途”的搜索分支再利用蒙特卡洛树搜索进行探索。数学里的“灵感”在这里被建模为对搜索空间的有效裁剪。2.5 大语言模型在数学中的位置大语言模型在数学任务上的表现常被误解。它可以流畅地写出数学证明草稿甚至能在很多标准化任务上给出正确答案但它并不具备对“正确性”的绝对判断能力。模型内部没有形式系统它的输出本质是“最接近训练数据中常见模式”的文本序列。因此大模型的最佳定位不是“最终裁判”而是“第一轮过滤器”它能把一个模糊的研究问题整理成清晰的分支结构能帮助快速生成证明草案也能把自然语言陈述翻译成形式化框架。但任何关键结论都必须交给证明器或严格的人工验证。3. 从“猜想”到“证明”AI 时代的证明流水线3.1 传统数学研究的闭环传统数学研究通常是这样运作的研究者凭直觉或实验观察提出猜想然后花费数月甚至数年寻找严格证明最后写成论文并投稿到期刊。论文发表后由两到三名审稿人阅读给出“认为正确”或“认为有问题”的结论。这个闭环最大的弱点是“验证”环节的不可靠性。审稿人也是人也会疲劳、误读、遗漏细节更重要的是当证明过长时没有人能真正逐字验证。数学史上出现过多次“发表多年后才发现证明有漏洞”的案例。这个问题的根源并不是审稿人不够负责而是验证工具太原始。3.2 AI 介入后的新闭环AI 时代的新闭环把验证环节彻底工具化。一条典型的流水线包括用符号计算或机器学习实验生成猜想用大语言模型辅助将猜想转化为形式化声明用证明助手、强化学习搜索或人工交互构造证明用验证器自动检查证明是否正确将证明与代码打包发布让全球社区共同维护。这个闭环中最核心的变化是“可复现性”从模糊的“我按你的思路重算了一遍”变成了“我用同一套证明脚本跑通了机器检查”。一个定理是否成立不再取决于它是否被某个权威认可而是取决于它能否在公开可执行的环境中通过验证。3.3 人机协作的三种典型模式在现阶段人机协作大致有三种模式。第一种是“人在环路中”AI 给出证明建议数学家判断方向是否合理再手动细化。第二种是“机器在环路中”数学家定义搜索空间和判定规则机器负责枚举大量分支自动化程度更高。第三种是“群体验证”多个独立的证明系统、多个研究团队同时对一个问题发起验证最终给出交叉确认。选择哪种模式取决于问题特征。竞赛几何、组合恒等式这类封闭问题适合机器主导搜索抽象代数、代数几何这类高度依赖概念重构的问题则更适合“人在环路中”模式。理解这三种模式就不必担心“AI 完全取代数学家”这类过于夸张的想象。4. 动手实践搭建一个最小的“AI 数学助手”4.1 环境准备下面通过一个小例子展示“AI 数学助手”的最小实现。我们不依赖某个具体云平台重点演示三个组件符号计算、形式化验证、大模型辅助推理。版本需要根据你的项目实际情况调整本文示例以常见环境为例重点演示配置思路。推荐环境如下Python 3.10 及以上用于运行 SymPy 和调用大模型 APILean 4 编辑器可选择 VS Code 配合 Lean 扩展一个大模型推理服务可以是 OpenAI 兼容接口也可以是本地部署的模型服务。安装 Python 依赖pip install sympy openai python-dotenv如果你使用本地推理服务只需把base_url指向本地地址即可不需要修改核心逻辑。4.2 用 Python 做符号计算先来看一个最简单的符号计算示例展开与因式分解。# 文件路径math_assistant/symbolic_check.py from sympy import symbols, expand, factor x, y symbols(x y) expr (x y)**2 print(展开结果:, expand(expr)) print(因式分解结果:, factor(expand(expr))) # 恒等式检查左边是否恒等于右边 lhs (x y)**2 rhs x**2 2*x*y y**2 print(恒等式是否成立:, lhs.equals(rhs))运行之后会输出展开结果: x**2 2*x*y y**2 因式分解结果: (x y)**2 恒等式是否成立: True在这个例子中equals方法内部会对两个表达式做代数运算并判断差是否恒为 0。它适合处理多项式、分式等场景用来快速验证猜想或排除明显错误的恒等式非常方便。4.3 用 Lean 写第一个形式化证明符号计算能发现“看起来成立”但不能代替严格证明。下面用 Lean 4 写出一个最小形式化证明。theorem two_plus_two : 2 2 4 : by rfl这个定理的意思是“证明 2 2 4”。rfl是“reflexivity”的缩写表示等式两边在定义上是相同的在 Naturals 的定义中2 是 1 的后继4 是 3 的后继计算 2 2 会得到 4因此反射性可以直接闭合证明。把这段代码保存为Examples.lean在 Lean 扩展环境中打开代码左侧会出现“No goals”或编译通过的提示。这是核心片段更复杂的证明需要引入 Mathlib 库且不同版本的语法会有差异。我刚接触 Lean 时容易产生一个误解既然rfl能证明 2 2 4那它是否也能证明所有简单算术答案是否定的。rfl只能处理定义相等的命题对于需要交换律、结合律的等式我们必须显式调用库里的定理或者使用omega、ring、linarith这类决策过程。import Mathlib.Data.Real.Basic -- 需要交换律才能证明a b b a example (a b : ℝ) : a b b a : by ring在这个例子中ring能够自动处理实数域上的交换律和分配律。但前提是导入 Mathlib并且 Lean 环境能够访问对应版本的数学库。如果你运行时报出unknown identifier ring多半是缺少导入或库版本不匹配。4.4 让大模型扮演“数学助手”大模型可以扮演证明思路的“讨论伙伴”。下面是一个调用 OpenAI 兼容接口的 Python 示例它向模型提出一个数学问题让模型先检查断言是否成立再列出证明骨架。# 文件路径math_assistant/llm_assistant.py import os from openai import OpenAI # 使用环境变量保存密钥本地服务可改成对应 base_url 与 model client OpenAI( api_keyos.environ.get(OPENAI_API_KEY, sk-local), base_urlos.environ.get(OPENAI_BASE_URL, https://api.openai.com/v1), ) prompt 你是一位数学助手。请根据以下要求回答 1. 先判断断言是否成立 2. 若成立写出证明骨架 3. 指出证明中可能存在的关键缺口。 断言对任意正整数 n有 1^3 2^3 ... n^3 (n(n1)/2)^2。 resp client.chat.completions.create( modelos.environ.get(MODEL_NAME, gpt-4o-mini), messages[{role: user, content: prompt}], temperature0.2, ) print(resp.choices[0].message.content)这里的关键设计是“先判断再给骨架再找缺口”。如果你只是简单提问“请证明这个等式”模型通常会直接生成一段漂亮但未必严谨的归纳证明。但当你要求它“指出关键缺口”时输出会更有鉴别价值。需要注意的是这段代码运行前请确认目标服务可用并且api_key、base_url、model_name都要按你的实际环境调整。不要把密钥硬编码到代码仓库里建议统一使用环境变量。4.5 运行与验证整体流程可以分为三步第一步用 SymPy 快速检查恒等式在小规模样本上是否成立第二步让大模型给出证明思路并指出风险点第三步把最终证明翻译成 Lean 代码交给验证器。为了让“验证”更可靠可以增加一个简单的穷举检查脚本对大模型给出的结论做数字采样验证# 文件路径math_assistant/sample_check.py def cube_sum(n: int) - int: return sum(i**3 for i in range(1, n 1)) def closed_form(n: int) - int: return (n * (n 1) // 2) ** 2 for n in range(1, 200): assert cube_sum(n) closed_form(n), ffailed at {n} print(前 199 个正整数均满足恒等式可以作为启发式验证。)必须说明穷举检查不是数学证明。它只能用来排除错误不能用来证明无穷多个情况。这就是后续需要 Lean 这类验证器的原因——机器不会因为“看起来都成立”就放行。5. 常见问题与排查思路5.1 形式化证明常见报错问题现象常见原因解决思路unknown identifier ring未导入 Mathlib 或运行环境缺少数学库增加 import或检查 Lean 与 Mathlib 版本type mismatch表达式类型不符合预期检查变量类型、声明定义逐步用#check查看类型goals accomplished但显示红色警告使用了不安全的 axiom 或sorry删除sorry补全证明Lean 无法编译环境版本太旧或缓存损坏升级到匹配版本清理缓存解决这些报错最有效的方式不是盯着错误提示猜而是从最小的例子开始增量构造。先证明rfl能处理的最小等式再逐步引入需要交换律的公式最后再上难度。5.2 大模型给出的数学证明包含幻觉大语言模型在数学上的“幻觉”几乎不可避免。它可能引用一个不存在的引理可能把一个错误符号写成看似合理的形式甚至在归纳证明中把“假设成立”和“证明成立”混在一起。最好的防御不是要求模型“不要出错”而是建立验证关卡先做数值采样再用符号计算检查最后用证明助手核验。当一条证明管线中只有“大模型生成”而没有“验证器把关”时不管模型多大输出都只能当作草稿。5.3 数学资料的版权与使用边界训练和评测大模型时数学论文是一个重要的数据来源但并非所有论文都可以随意爬取和复制。arXiv 上的论文大多允许非商业使用但仍有明确许可协议出版社论文的版权通常掌握在出版方手中。在工程实践中应尽量使用开源数学库和带明确授权许可的数据集不要为了训练一个内部模型去大规模抓取未授权的受版权保护论文。对于以“最小可用”为目标的个人项目优先使用公开 API 或已授权的开源模型即可。5.4 如何选择工具链如果你是刚起步建议从轻量组合开始SymPy 负责代数运算Lean 负责形式化验证一个可访问的大模型接口负责讨论和翻译。不要一开始就搭建完整的大规模训练基础设施这会把大量时间花在非数学问题上。当项目进入稳定期后再考虑引入本地部署模型、自建测评集、自动化 CI 验证等工程手段。重点不是把所有工具塞进一个系统而是保证模型中每个组件都有“可验证的下游”大模型的输出必须有符号系统或证明器接受否则它只是生成了一堆文本。6. 数学家的新角色与工程建议6.1 从“解题者”到“问题设计师”“英雄时代”的落幕并不等于数学不再需要个体能力。更准确的描述是数学家的核心竞争力正在从“我能亲手算完这一大步”转向“我能定义出值得自动化求解的问题”。当一个证明的主要步骤可以被机器搜索、验证和支撑时研究者最独特的贡献反而不是某个细节技巧而是对问题结构的理解、对抽象层次的把握以及“把直觉转化为可验证规格”的能力。这其实就是一种工程能力把模糊的数学问题拆解成计算机能参与处理的任务。6.2 把证明变成可执行产物在传统的论文发表模式中读者拿到的是排版好的 PDF里面是一整套自然语言描述。真正想复现的人必须手动跟随作者思路完成非常耗时的推演。AI 时代的论文可以做得更好把证明源文件、构建脚本、测试用例一并提交到代码仓库。建议在项目中使用版本管理工具管理证明文件每次变更都自动运行验证器。一个简单的 CI 工作流可以这样构建推送新证明后自动编译 Lean 文件运行测试脚本收集符号计算检查结果最后生成一份可读的报告。这能让“形式化验证”成为项目持续集成的一部分而不是论文之外的一次性工作。6.3 工程实践建议代码与证明文件混在一个仓库时工程规范会直接影响维护成本。下面几条建议尤其值得重视配置管理模型 API Key、base_url、模型名全部放入.env或环境变量不要写死在代码中异常处理网络请求要做超时重试验证器报错要保留上下文日志安全边界AI 生成的代码不可直接运行尤其是涉及文件系统、网络、系统命令的代码必须经过人工审查并在隔离环境中测试版本锁定Lean 与 Mathlib 的版本高度耦合建议锁定版本并用 lockfile 管理 Python 依赖命名规范证明文件与论文章节一一对应尽量做到“看到文件名就知道对应哪个定理”。以上每一点都是在长期维护数学项目时容易踩坑的地方。尤其是“AI 生成代码”的安全边界不能因为代码看起来能编译就盲目运行。6.4 对学术出版与审稿的影响当证明可以形式化、可以机器验证之后学术出版的标准也会随之变化。未来很可能出现一种新的审稿模式论文投稿时同步提交形式化证明附件编辑先跑一遍验证器再请专家判断“这个问题本身是否重要、方法是否有启发性”。这并不会取消人工审稿而是把审稿工作从繁琐的细节检查中解放出来让专家把精力放在更根本的问题上。审稿人的价值不再是逐字核对推导而是判断研究方向的创新性和概念层面的正确性。7. 总结与学习路线7.1 核心要点回顾本文围绕“AI 是否终结了数学的英雄时代”展开核心可以概括为三点。第一数学研究正在从个体灵感中心化的模式走向多方参与、容器化验证的网络模式。第二AI 在数学中最真实的角色是验证器与搜索器的组合而不是“突然会证明一切”的超级模型。第三对普通开发者来说现在就能通过 SymPy、Lean 和大模型 API 搭建一套最小可用的数学辅助与证明工具链。7.2 下一步学习路线如果你刚开始接触这个方向我建议按下面的顺序推进第一步用 SymPy 复现本文中的符号计算示例熟悉expand、factor、equals的能力边界第二步在 VS Code 中安装 Lean 扩展从rfl和简单定理开始逐步编写自己的证明第三步阅读一个已形式化的开源数学项目观察数学证明如何被拆成可维护的模块第四步尝试用大模型辅助翻译一段论文中的自然语言证明再用 Lean 验证它是否正确第五步关注自动形式化工具和 Mathlib 社区的最新进展及时更新自己的方案。这个路线不需要做大规模投入核心是建立“生成-验证”的闭环意识。真正有价值的不是让模型说出一个漂亮结论而是让验证器能持久地接受这个结论。7.3 给实践者的最后提醒数学的“英雄时代”并不是被某一次技术突破突然终结的。它是被一个漫长而坚定的工程化进程逐步重塑的符号计算先承担了繁琐的代数操作证明助手再接管了严谨性验证大模型的出现则进一步降低了从自然语言到形式语言的转换成本。当你愿意从一个最简单、最底部的证明开始慢慢把它扩展成可复现、可验证的工程项目时“世界心智”对你就不再是一个抽象概念而是一个你正在参与其中的真实现实。这也正是这个时代最值得期待的数学实验方式。