数学研究最近几年被 AI 连续冲击了好几次AlphaTensor 重新发现了更省的矩阵乘法算法AlphaGeometry 在欧氏几何上逼近国际数学奥林匹克金牌选手FunSearch 在组合数学的 cap set 问题上给出了新的构造边界。这些工作的共同点是AI 不是简单扮演“计算器”而是深度参与“探索—假设—验证”的研究循环。于是有很多人在问一个更根本的问题AI 会不会逼着数学家重新定义自己的学科Ask HN 上就出现了这样一个讨论标题“社会是否因为强迫数学家重新发明自己的领域而走运了”这个问题的有趣之处在于它不是问“AI 能不能做数学”而是问“当学科的核心产出方式——证明与发表——被新工具打乱之后从事这个学科的人会失去什么、得到什么”。国内技术社区里讨论跑模型、调参、看显存的内容很多但从这个角度把“AI 改变一门学科的研究生态”讲清楚的文章比较少。这篇就把问题拆开结合形式化验证工具和 AI 辅助证明的实际状态聊一聊数学家“被迫重新发明”这件事到底是悲剧还是红利。本文会先拆解标题里“强迫”和“重新发明”到底指什么然后介绍目前 AI 参与数学研究的几类主流路线再演示一个最小可运行的“Lean 形式化证明 大模型生成思路”工作流最后给出一份适合程序员和技术研究者参考的判断清单。无论你是做 AI 工程、关注数学软件还是单纯好奇“人脑证明”和“机器验证”未来怎么共存这篇文章都会给你一个可复用的分析框架。1. 拆解标题“强迫”和“重新发明”到底指什么先看“强迫”。这个词听起来像是外部强权在推动但如果对近五年数学与 AI 的交叉进展有所了解会发现真正的压力来自技术本身。传统的数学研究依赖黑板、草稿纸、LaTeX 论文和同行评审证明以自然语言写成可读性优先严谨性靠领域内专家的集体审查来保证。这套机制运行了几百年但它有两个致命的慢第一证明过程无法被机器直接执行很多“显然可得”的跳步在几年后会被发现是错的第二一篇论文的验证周期太长审稿人通常只能抽查关键引理而不是从头到尾重推全篇。当 AI 研究开始介入情况变了。AI 可以快速生成候选结论可以枚举大量构造可以尝试各种辅助线或变换路径。但这些输出不是传统意义上的“论文级证明”而是“可能成立的思路”或“程序可检查的构造”。数学家如果想利用这些能力就不能再只靠黑板和直觉必须学会把问题翻译成机器可验证的语言必须习惯“结论先由模型猜出来、再由证明器或人证出来”的新节奏。这就是“强迫”的真实含义——不是有人逼你而是新的生产能力出现之后旧方法在效率上打不过了。再看“重新发明”。数学知识本身不会被推翻112 不会变成 3黎曼猜想如果被证出来也还是同一个黎曼猜想。真正被重写的是研究的工作流、产出形式以及“什么才算足够严谨”的判定标准。过去一篇论文写完证明基本上就结束了现在越来越多研究团队会把关键引理放进 Lean、Coq 或 Isabelle 这类证明助手里做形式化验证把“口头共识”变成“可执行事实”。这个过程已经不是边缘实验而是正在成为部分领域的主流工程实践。对程序员来说这个场景并不陌生。当编译器、类型系统、静态检查工具一层层接管代码工作之后程序员的工作重心从“写出能跑的代码”变成了“设计清晰的结构并判断验证结果是否符合意图”。AI 编程助手出现后这个趋势更明显。数学界正在经历的恰恰是软件工程十几年前经历过的那次转型。所以这不是一个遥不可及的学术话题它和我们每天面对的工具链进化是同构的。2. 数学家的工作方式正在被 AI 改变三类代表系统要理解“重新发明”的实质不能只看概念要看具体的技术路线。目前 AI 参与数学研究大体可以分成三类每一类解决的是不同类型的数学任务也对应不同的验证策略。2.1 强化学习驱动的算法发现AlphaTensorAlphaTensor 把矩阵乘法算法搜索建模成一个单人的棋盘游戏状态是当前矩阵分解的剩余项动作是选择某种秩 1 更新奖励是乘法次数的减少。通过强化学习训练它找到了比传统 Strassen 类方法乘法次数更少的矩阵分解方案。这类工作的意义在于AI 搜索空间远超人工构造能覆盖的范围而且最终结果可以被严格验证——矩阵乘法公式一旦写出来代入计算即可验证是否等价。它代表的是“AI 做技术性优化”的路线相当于是把一个离散优化问题暴力搜索到一个此前没人找到的角落。2.2 大模型与进化搜索结合的探索FunSearchFunSearch 的思路更接近“AI 生成候选验证器做守门员”。它先让预训练 LLM 根据问题描述写出一段能找到目标构造的程序再用自动评估器检查这段程序生成的数学对象是否满足约束条件满足的保留不满足的丢弃然后反馈给模型迭代进化。这个流程的关键在于模型本身不需要直接输出正确答案它只需要不断提供“有点希望的候选程序”最后真正把关的是自动验证器在有限域上的硬性检验。这种模式在组合数学等存在大量搜索空间的领域已经拿到新结果但读者要注意有限域上的验证和一般性证明之间还有距离所以 FunSearch 的结果要变成正式定理仍然需要人的跟进。2.3 神经符号方法做几何推理AlphaGeometryAlphaGeometry 则结合了语言模型和符号推理引擎。它先通过合成数据训练一个能生成辅助线和构造步骤的模型再用专门的符号推理引擎对这些步骤做闭环验证把“模型提出的构造”和“规则引擎能推出的结论”反复对齐。官方发布的结果是在欧氏几何问题上达到了接近 IMO 金牌选手答题水平的成绩。几何问题天然适合这种模式因为辅助线的选择是典型的启发式搜索问题符号引擎又提供了严格的检查。它代表的是“AI 猜构造、机器验步骤”的混合推理路线也是目前看起来最接近数学家真实工作方式的一种。三类系统的共同点值得专门说一句它们都不再把“给出一篇完整的自然语言证明”当作唯一目标而是把“在一个可验证的框架内得到一个有效结论”当作目标。这种从“文本说服”到“可执行验证”的重心转移才是数学家被迫重新发明自己领域最核心的变化。3. 形式化证明工具正在把“黑板思维”推进压力测试区AI 参与发现只是故事的一半另一半是证明的交付形式。如果 AI 给出的结论永远停留在文本说明那么它顶多算高级的“数学搜索引擎”无法真正进入研究闭环。但形式化证明工具改变了这一点其中最典型的例子就是 Lean 4。3.1 什么是形式化证明形式化证明把数学陈述编码成逻辑规则、类型规则和计算规则由证明助手逐步检查每个推导步骤是否合法。和传统自然语言证明的最大区别是机器必须执行每一个推理步骤任何一步跳不过去你的证明就被打回。这个过程中大量“显然”“易得”“同理”会被证明是站不住脚的抽象。对数学家的冲击是双重的一方面证明的可靠性大大提高另一方面原本依靠默契和直觉的宽松论证方式彻底失效。3.2 Lean 4 的最小可运行示例Lean 是微软研究院发起、社区持续推进的交互式定理证明器Lean 4 目前是主流版本配合大型数学库 Mathlib已经形式化了相当多的基础数学。这里给一个最小的 Lean 4 示例不需要任何数学库就能跑通-- 最小定理证明1 1 2 example : 1 1 2 : by rfl这段代码看起来短得不像数学但它背后是类型检查和计算归约Lean 会将左端的1 1按照 Nat 的加法定义逐步归约到2然后发现两边定义相等rfl战术直接关闭目标。第一次看到这个画面的人通常会意识到过去在黑板上一笔带过的推导在证明器里是一条精确的、需要被机器确认的计算路径。更复杂的定理则需要借助induction、rewrite、omega等大量战术库学习曲线很明显但循环一旦建立从“人看懂”到“机器验证”之间的鸿沟就被填上了。3.3 为什么不所有数学家都转向 Lean既然 Lean 这么好为什么没有立刻统治学术界原因很现实第一形式化一份成熟的证明往往比写原始证明慢得多很多研究者根本没有这个预算第二目前自动化战术对数学分析、几何、代数几何等方向的支持分布很不均匀有的领域形式化顺畅有的领域每一步都很痛苦第三传统同行评审和职称评价不认“你审了别人证伪了一堆漏洞”这种贡献形式化工作被当作翻译活的偏见依然存在。这些阻力决定了“重新发明自己的领域”不是一朝一夕能完成的。3.4 形式化对研究的真实价值我个人的看法是形式化的价值不在于让所有数学家都改行写 Lean 代码而在于它创造了一个“可执行的证据锚点”。当你把论文里的关键引理用 Lean 形式化之后再难的问题都被拆成了机器看得懂的小步推理任何真正逻辑断裂都会暴露无遗。这种“暴露”恰恰是 AI 时代最需要的能力——因为大模型生成证明思路时最容易犯的错误就是用一个看似流畅的陈述掩盖真正的逻辑缺口。证明器就是专门拆穿这种假流畅的仪器。4. 当 AI 成为数学合著者机会与隐患把 AI 引入数学研究机会和风险都很明显。先说机会AI 在枚举候选、搜索反例、构造复杂例子上具有天然优势。一个组合的问题人工可能只能试几十种配置AI 可以试几十万次并自动筛选出值得人类注意的对象。一个需要添加辅助线的几何题传统解法依赖经验AI 可以基于大量合成样例给出非直觉的构造路径。这些都是实打实的研究加速。但隐患同样突出。大模型的底层逻辑是概率预测没有内在的数学正确性约束。它可能用流利的自然语言描述一个根本不成立的证明每一句都像模像样整体却是空中楼阁。更危险的是如果研究者把模型输出误当成“经过检查的答案”就会重新引入几十年前计算机辅助证明刚出现时的那种焦虑机器的结论是否可信人类要不要再去验证一遍。这个问题在四色定理时代曾经争论过几十年AI 时代只会更尖锐。因此目前最稳妥的思路是把 AI 定位成“猜想的生成器”而不是“证明的终结者”。AI 负责提出可能成立的命题、给出辅助线、缩小搜索范围人负责解释哪些候选值得追证明器负责把追到的结论落成可执行证据。换句话讲AI 解决的是“哪里可能有金子”人类和证明器解决的是“这块金子到底是不是真的”。站在社会层面“走运”与否其实取决于能不能建立一个高效的分工协作机制。如果人类把 AI 的输出直接等同于真理数学的公信力会崩塌如果人类善用 AI 挖掘直觉、同时用证明器严格把关数学研究的生产效率会迎来一次飞跃。四色定理的争议最终被数学界消化AI 辅助数学大概也会走一条类似的曲线先震惊、再怀疑、再局部接受、最后变成常规工具。5. 编程领域已经先走了一遍我们才是被逼迫最久的人讨论数学家被 AI 逼迫程序员其实是最有发言权的群体。过去二十年编译器和类型系统就在持续做一件事把程序员的“自由表达”部分地约束成机器能检查的规则。C 的指针可以让任何内存变成任意类型Rust 的类型系统直接告诉你很多操作不能写JavaScript 的动态类型跑起来方便TypeScript 用编译期检查换可靠性。每一次约束收紧都有开发者抱怨“重新发明自己的领域”但最终的赢家是那些顺应工具变化、把精力转移到更高抽象层面的工程师。AI 编程助手把这件事推到了新高度。今天用大模型生成代码已经被很多团队当作常态。程序员的工作从“逐行写代码”变成“给出需求、评审生成结果、修正错误、补齐测试”。这个转变里程序员的判断力和测试意识成了最稀缺的能力。数学家在 AI 时代面临的情况几乎完全一样正在从“手写证明”变成“提出命题、评估 AI 生成思路、用证明器或人工核对关键步骤”。区别只是数学对“验证”的要求比工程对测试的要求严格得多。程序员先被逼迫的好处是我们给数学家留下了一套可以借鉴的工程方法论用版本管理记录实验和生成参数用自动化测试验证功能用 code review 做同行评审。数学家不需要把这些方法照搬但“可重演、可检查、可回溯”这些原则完全可以转移到证明与 AI 协作的工作流中。换句话说被迫改变并不一定是坏事关键是你能不能建立起一套配套的新方法论而不是停留在抱怨内卷和危机感的阶段。6. 实操从零体验“AI 数学”的最小工作流说了这么多理论落到实际操作才更有说服力。这里给一套最小可运行工作流用 Lean 4 做形式化验证用大模型生成证明思路最后把二者串成一条“AI 猜、证明器证”的流水线。整个流程只需要一台能跑 VS Code 的电脑不需要高配 GPU。6.1 环境准备先安装 Visual Studio Code然后在扩展市场里搜索并安装 lean4 扩展。Lean 工具链本身建议通过 elan 安装官方安装脚本以项目官网为准。安装完成后打开任意.lean文件Lean 自动检查语法和证明状态。第二步是准备模型服务可以是一个本地兼容 OpenAI 的推理服务也可以直接用公共 API按你手头的环境决定。核心是确保代码里能通过一个chat.completions接口发送提示词并拿回文本。# 创建 Lean 项目示意 lake new my_first_math cd my_first_math# 在 VS Code 中打开项目然后新建 Test.lean # lean4 扩展会自动加载项目环境并开始检查文件6.2 写第一个 Lean 证明在项目中新建一个.lean文件写入最小证明-- 最小定理证明1 1 2 example : 1 1 2 : by rfl保存后Lean 窗口会在右侧显示“No goals”证明通过。可以试着把它改成1 1 3右侧立刻报错这就直观地体验到了“机器强制验证每个式子”的约束力。想再进一步可以尝试证明自然数加法的结合律这个要拆成归纳证明语法稍微复杂需要查一下 Lean 的 tactic 文档但值得花半小时跑通一次因为它能帮你建立“证明就是程序”的手感。6.3 用大模型生成候选证明思路下面用 OpenAI SDK 风格写一个标准调用示例。这个示例是通用模板具体的base_url、model和api_key必须替换成你实际服务环境的值本地推理服务通常用http://127.0.0.1:8000/v1这类地址模型名以你实际部署的权重为准from openai import OpenAI # 以本地 OpenAI 兼容服务为例具体地址按环境替换 client OpenAI( base_urlhttp://127.0.0.1:8000/v1, api_keyEMPTY, ) resp client.chat.completions.create( modelqwen2.5-math, # 替换为实际可用的模型名 messages[ { role: system, content: 你是数学助手只输出证明思路不编造未经验证的断言。, }, { role: user, content: 请给出证明 sqrt(2) 是无理数的关键步骤尽量简短。, }, ], temperature0.2, ) print(resp.choices[0].message.content)这个流程能做什么你可以把“请给出证明步骤”的提示词换成“请给出某条引理可能的证明思路”然后把模型的输出当成候选思路自己或在 Lean 中手工验证关键步骤。注意temperature尽量设低0.2 左右减少模型自由发挥的程度。如果你需要生成多个不同方向的探索再适度调高。6.4 把两者接成最小流水线一个非常低成本但完整的工作流是这样先让大模型生成证明思路生成的结果只是“可能性”再把关键引理用 Leanexample写出来用by后的 tactic 逐步验证如果 Lean 过不了把报错信息返回给大模型让它修正思路迭代若干轮。这个循环和主流研究团队的方式在原理上完全一致只是规模小得多。通过这个最小闭环每个读者都能理解为什么说“模型负责猜、证明器负责证”。整个流程跑下来的第一个体会一定是真正消耗时间的不是让模型生成而是把 idea 写成 Lean 能接受的证明脚本。这个消耗不是浪费它逼迫你把证明里的每个“显然”都重新审视一遍。7. 常见误区和排查思路AI 与数学结合的讨论里微信群里常见的误解非常多。下面这张表把几个高频误区和对应的处理方式整理出来方便直接对照。误区现实建议AI 说“该结论成立”就等于成立大模型是概率模型没有数学正确性保证所有结论必须有形式化验证或人工复核Lean 能快速证明一切数学定理真实数学证明需要大量交互式引导和战术调试先做小引理再逐步扩大范围形式化工作只是把论文翻译成代码形式化过程经常暴露原始证明中的逻辑漏洞把它当成找漏洞的测试而不是翻译活有了 AI 和证明器数学家会失业提出值得研究的问题才是最稀缺的能力重点训练问题意识和方向判断用 AI 就能完成科研闭环验证器和人工复核缺一不可建立模型验证 证明器验证的双重机制排查方面给几个高频问题快速处理方案。模型输出不一致先降temperature然后多次采样找共识如果依然不稳定就把任务拆成更小的子问题分别问。Lean 报错时先看右侧的 goal 状态确认当前需要证明的目标到底是什么再决定是rfl还是rewrite还是induction。形式化一个真实定理耗时太长可以采用隔离策略只形式化论文中最重要的三个引理而不是全篇文章。批量处理思路时给每条生成结果加一个可回溯的编号记录模型名、参数、prompt 和日期避免事后找不到来源。事实上所有坑的根源都可以归结为一句提醒把大模型当参考者不要当裁判。8. 最佳实践给想入局的人四组建议如果你被这个方向吸引打算在自己的工作流里引入“AI 猜 机器证”的模式下面这几组建议值得直接收藏。第一组是模型与验证层面。不管用什么模型先找一种可验证的兜底手段。数学题可以用 Lean算法题可以用测试用例组合构造可以用暴力验证器。模型输出永远只是“候选”验证器通过后才能叫“结果”。这个习惯养成之后AI 的幻觉问题对你的杀伤力会大幅下降。第二组是研究策略层面。第一次尝试不要选一个大定理选择你平时就很熟悉、但一直没有严格写出每一步的小引理把它在 Lean 里形式化一遍。这个小成功会帮你建立完整的心智模型什么样的证明能让机器通过什么样的中间步骤需要补遇到报错应该去哪里查。先复现一个小结论再扩大边界比一次性挑战大问题要高效得多。第三组是工程协作层面。AI 实验和证明脚本都要纳入版本管理。prompt、模型参数、输出结果、Lean 脚本一起提交方便回滚和复盘。做批量探索时为每个任务建立独立的输入输出目录处理好失败重试和日志记录。这不是写论文的人该不该学工程的问题而是未来跨学科合作的标配能力。第四组是职业发展层面。不论你是数学家、AI 工程师还是普通技术人员单纯比拼“手写证明”或“手写代码”的上限都会越来越低真正的竞争力在于定义问题和判断答案。平时可以有意识地训练自己面对一个模糊问题能不能拆成可验证的小步骤面对一个 AI 输出能不能快速定位最可疑的断言。这个问题意识和判断力才是 AI 时代最稳固的护城河。9. 总结“走运”还是“考验”取决于我们怎么接招回到 Ask HN 那个问题社会到底有没有因为强迫数学家重新发明自己的领域而走运目前最稳妥的判断是AI 并没有让数学研究变简单它只是把难题从“如何证明”转移到了“选择什么问题值得证明”。数学家在形式上被逼着接纳机器验证在策略上被逼着接纳 AI 作为探索伙伴这个过程有阵痛但机会也非常明显。对读者来说这篇文章最值得立刻动手验证的一件事不是去追前沿论文而是把文章里第 6 节的最小工作流跑通装好 Lean 4写一个1 1 2的证明再让大模型生成一个无理数证明思路然后花一点时间用 Lean 验证它。这个极小的闭环一旦建立你对“AI 该怎么用到高严谨领域”的理解会超过读一百篇讨论文章。最容易踩的坑是误把大模型的流畅表达当成数学证据记住一个原则就行凡是不能被验证器或严格手工验算接住的结果都只是灵感不是答案。文章建议收藏备用等你自己跑通最小示例后再回来看第 8 节里的建议体会会很不一样。下一步可以关注的方向包括Lean 社区里不断扩大的 Mathlib 数学库以及将大模型输出直接转成 Lean tactic 的自动化工具。真正“重新发明领域”的人不会是被动等待规则改变的旁观者而是主动把新工具接入自己工作流的那批研究者。