过去三年里我观察到一个很有意思的现象身边的数学同行分成两拨一拨人焦虑AI会抢走饭碗另一拨人觉得AI工具不过是个高级计算器连正眼都不看。这两种态度我都经历过直到最近认真读完Daniel Litt那篇长文才意识到问题问错了。真正该问的不是“AI能不能证明定理”而是“当机器能把证明过程做得又快又好人类数学家还剩什么不可替代的价值”。Daniel Litt是搞代数几何的数学家他对这个问题的判断很直接——未来数学研究的核心产物会从“定理证明”转向“人类理解”。这不是说证明不重要了而是说证明会像今天的四则运算一样变成一项可以被外包、被工具化的基础能力。真正困难的、值得数学家投入精力的事情是搞清楚一个数学对象为什么长成这样、它和其他领域之间有什么隐秘的联系、用什么方式讲述才能让结构变得透明。这篇博文就想把这个判断掰开揉碎讲讲AI时代数学实践到底会怎么变什么会被替代、什么不会以及一线的数学工作者要怎么调整自己的工作流。这个话题值得展开的原因很现实。今天任何一个学数学的学生都能用AI辅助做习题、查文献甚至验证自己的猜想但这个领域的信息噪声极大很多人在用AI做数学时踩了坑还不知道。我把Daniel Litt的观点结合自己用Lean、用大语言模型、做数值实验的实操经验整理成一套思路希望能帮到正在使用AI工具的数学系学生、科研人员和关注科研方式变革的从业者。1. 核心思路拆解证明与理解正在被解耦1.1 一个反直觉的预测证明变得越容易理解反而越值钱先讲一个容易被误读的地方。Daniel Litt并不是在说AI会摧毁数学他说的其实是相反的事。过去两千年数学共同体默认“证明”和“理解”是同一件事的两面——你想理解一个对象就必须亲手把一个证明写出来写不出来就说明你没懂。这个协作模式在历史上很有效但它有一个隐藏的成本大量优质的数学精力被消耗在“把直觉转译成严格形式语言”这一步上而真正的理解反而可能发生在转译之前。AI出现之后事情开始起变化。像Lean 4、Coq这类形式化验证工具加上以GPT-4为代表的大语言模型已经能把“把证明写出来”这件事做得越来越自动化。Daniel Litt的核心判断是一旦这个转译环节不再需要人类亲手完成数学家的工作重心就会自然地向“形成理解”倾斜——你需要知道往哪个方向走、什么结论值得信、怎么给机器下指令去验证而不是亲自把每个逻辑链条都写完。用工程来类比就很好懂。CAD软件普及之前结构工程师要花大量时间画图图纸本身既是沟通工具也是思考工具。CAD普及之后画图变得极其高效但工程师的核心竞争力反而回到了力学概念和结构方案上——软件替代的是绘图员的活不是设计师的活。数学领域的AI也在走同样的路。1.2 被替代的是“转译劳动”不是“数学直觉”这里我需要澄清一个常见的误区。很多人一听“AI证明定理”第一反应是“以后数学家没用了”这个判断是错的。理解这件事应该拆成三层第一层逻辑验证层。一个证明是否完全严格、每一步是否符合形式规则这是最容易被机器替代的部分。今天的Lean等系统对这部分已经做得很不错用户只需要给定理声明剩下的步骤能在交互式环境中逐步补全。第二层问题构建层。一个领域有哪些重要的未解问题哪个猜想值得投入三个月时间去研究两个看起来不同的数学对象之间是否可能存在深层联系这层很难被机器替代因为问题的价值判断依赖人脑对领域全局的把握和品味。第三层概念理解层。为什么这个定理成立的条件恰好是这些如果把某个假设去掉会出现什么有趣的反例这个定理放到另一个理论框架里能获得什么新解释这层需要人脑做大量的类比、隐喻和视觉化思考。Daniel Litt说的“从证明定理转向人类理解”本质上就是把数学家的劳动从第一层解放出来逼着大家把精力真正投到第二层和第三层。这不是妥协而是一种解放。事实上有经验的数学工作者都知道大量日常工作是枯燥的化简、代入、检查边界条件这些工作耗时最多对创造性反而没什么帮助。如果AI能把这部分接过去研究者每天能腾出至少三到四个小时思考更本质的问题。1.3 从“产出证明”到“构建解释”数学文档的形态变化顺着这个思路往下推数学论文的形态也会变。现在的数学论文实际上是一个线性的证明流定义引理定理证明推论。这种格式高度标准化非常适合人类审阅但它有一个很大的问题——它把整个思考过程中真正精彩的“为什么”压平了。很多论文上去看每一步都对但读者照样不知道作者当初是怎么想到这个思路的。AI时代数学文档开始转向“多模态解释”和“交互式验证”两个方向。一方面论文可以配可执行代码块让读者在浏览器里直接改动参数看结果另一方面证明的核心部分可以对接Lean等系统读者能展开交互式检查而不需要盲信作者。这种变化实际上在倒逼数学家把“为什么这样想”作为一等公民来对待——因为证明细节可以被机器接管作者就有余裕去写通顺的motivation、讲清楚类比和试错过程而不是把所有篇幅都留给严格的逻辑链。2. AI数学工作台核心工具盘点与选型逻辑2.1 工具分三层别指望一把锤子砸所有钉子我刚接触AI辅助数学的时候走过弯路总想找一个“万能工具”解决所有问题。实际用下来发现现在这个阶段AI数学工具已经明显分化成三层每一层解决不同的问题用混了就会很痛苦。第一层是形式化验证系统代表是Lean 4、Coq和Isabelle/HOL。这类系统的核心能力是“保证证明无懈可击”。你写一段代码式的证明脚本系统会用严格的类型理论去检查每一步推导直到整个证明通过编译。它的优点是完全可靠缺点是学习曲线极陡、写证明速度慢。我自己的体验是一个在大学教材上只要半页纸就能写完的简单定理在Lean里可能要写上百行而且头几周基本都在跟语法搏斗。第二层是大语言模型辅助工具代表是GPT-4、Claude这类通用模型也有一批专门做数学和代码生成的模型。它们的能力是“快速生成一个看起来合理的起点”。你描述一个你不确定怎么做的问题它能给出一个思路框架甚至把关键公式、反例条件都列出来。优点是快缺点是它不保证正确幻觉比例不低尤其是涉及具体数值和进阶数学分支的时候。第三层是自动推理与计算探索工具代表是Mathematica、SageMath、Z3求解器以及各种针对特定问题写的计算脚本。它们负责的环节是“把模糊直觉变成可测试的具体数据”。比如你猜某个不等式成立先用高精度数值在这类工具里扫一圈看看有没有反例有反例就省得白费力气证明没有反例再往严格证明方向努力。这类工具的逻辑不是“证明”而是“排除错误猜想”和“给证明方向提供线索”。三层工具的关系不是替代而是分工。我的建议是把它理解成一条流水线大语言模型负责出活计算工具负责筛选活形式化系统负责给最终可靠的证明兜底。2.2 Lean 4是当前最值得投入的形式化系统如果你只打算学一个形式化验证工具我的建议是Lean 4。原因有三个。第一Lean 4背后有Mathlib这个巨大且活跃的数学库里面已经形式化了大量基础数学结果新手不用从零开始证明一切可以直接引用前人建好的模块第二Lean社区建设得比较好教程、讨论、在线游戏都齐全入门体验比Coq当时好太多第三Lean的语法更接近现代函数式编程对接触过编程的人非常友好。不过我要提醒一句别把Lean当计算器它是验证器。它的工作方式是“你给它一个证明脚本它检查你写对了没有指出哪儿有漏洞”。也就是说你先得有思路Lean负责把关。很多新手碰壁是因为不明白这个逻辑以为把问题丢给Lean它就能自动想出证明——目前还做不到至少做不到通用级别的自动推理。2.3 大语言模型的选择与边界数学场景下用大语言模型我的建议是不要把通用聊天模型当唯一选项要按任务分。做概念解释、文献梳理、思路对话用通用模型GPT-4那一档或者Claude、Gemini就行它们的数学直觉和语义理解已经相当够用。但要让它做具体的符号推导或写Lean证明建议换用专门针对数学/代码微调的模型比如DeepSeek在数学推理上的表现就很好还有一批Math Specialist模型也能应付常规推导。另外要明确一个边界大语言模型在数学上的定位是“同行评议者”而不是“权威导师”。它给出的任何一步推导哪怕看着再合理都要带着怀疑去检查。我见过很多次它在证明过程中悄悄偷换条件或者在二阶以上的逻辑判断上出现明显矛盾而你如果不逐行校验很容易被它带进沟里。判断一层意思和判断一个数学证明是两回事。3. 实操流程从形成猜想到得到可验证的结果3.1 完整工作流的五个环节这一节我把实际操作过程完整拆开讲。假设现在摆在面前的是一个研究级别的问题比如想知道某个递推序列的增长率是否满足某个渐进估计。传统做法是直接坐到书桌前开始推算AI辅助之后的流程完全不同。第一步把问题精确化。这一步看起来不起眼占我整个工作流大约四分之一的时间。你要把模糊的数学直觉转成严格的问题陈述变量范围是什么参数依赖哪些不变量期望的结论是相等、不等式还是构造性存在这个阶段我通常会和语言模型来回对话让它帮忙找出陈述中不够精确的地方。语言模型很擅长做这个因为你给它一段有歧义的问题描述它会追问边界条件。第二步生成探索思路。把问题陈述丢给语言模型让它给出3到5个可能的证明方向并且要求它对每个方向说明“为什么你觉得这个方向行得通”。这个阶段不要指望它给出最终答案而是利用它帮你打开思路。它可能会提到一个你没想到过的经典定理或者一个关联领域的技术集。即使思路是错的也能帮你排除掉部分路线。第三步数值与符号实验。拿SageMath或者Mathematica把猜想中涉及的小规模案例全部跑一遍。这步是真正的筛选器。我个人的经验是至少三分之一的猜想在这一步就死了——你很快发现某些边缘情况根本不满足不等式这时就要回头修正猜想而不是硬证。第四步严格证明。从一个经过数值检验的修正版猜想出发开始推导严格的证明框架。理想状态下这个框架就是最终论文的大纲只是把细节补全而已。如果在这里卡住我会再回到语言模型把当前的结论和卡住的原因讲给它请它给出一个可能的拆解路线。第五步形式化验证。如果你想确保结论万无一失且有充足的预算和时间可以把证明的关键模块用Lean或Coq做形式化。这一步适合重要引理、核心定理不适合几百页的整篇论文。对多数探索性研究我认为做到第四步就够了形式化验证是锦上添花。3.2 我用Lean验证一个简单定理的完整过程为了让你对形式化验证有一个直观感受这里放一个入门级Demo。假如我们想验证一个非常基础的结论若n是偶数则n²是偶数。在Lean 4里代码可以这样写import Mathlib.Data.Nat.Parity import Mathlib.Tactic example (n : ℕ) (h : Even n) : Even (n ^ 2) : by rcases h with ⟨k, hk⟩ use 2 * k ^ 2 calc n ^ 2 (2 * k) ^ 2 : by rw [hk] _ 2 * (2 * k ^ 2) : by ring简单解释一下逻辑Even n的定义是存在某个自然数k使得n 2k。证明的思路是把n替换成2k那么n²就是(2k)²化简成2 * (2k²)这正好说明n²是某个数的两倍也就是偶数。第一行rcases把“存在k”这个信息拆出来第二行use给出一个候选的witness也就是2*k²最后用calc块完成等式推导ring策略处理代数化简。这个例子很小但能让新手明白Lean的工作方式它不是自动证明而是检查你给的每一步是否合法。我头一次从零写完这个证明大概用了二十分钟大部分时间花在查语法和找库函数上。真正对这个过程有体感之后你会明白形式化验证的瓶颈是“人把证明翻译成机器的语言”而不是“机器验证的速度”。3.3 如何用语言模型快速搭一个研究脚手架大语言模型在数学研究中的真正价值不是直接给出最终定理而是帮你在一个新领域快速建立起脚手架。我常用的一个提示词模板是我先用一两段话描述问题背景和已知条件。我请求请从三个不同角度给出可能的解题思路每个思路都注明它的优势、可能的风险和适用的经典工具。我希望你以“同行讨论者”的语气回应不要给确定性结论而是给出需要我进一步验证的工作假设。这样得到的回答通常会比直接问“怎么解这道题”有用得多。原因是它迫使模型进入探索模式而不是答案模式。数学研究本质上是探索性的如果你用查询的方式和它互动得到的往往是一块漂亮的拼图碎片而不是完整的图纸。用探索式的提示词你获得的是一个可以拿着继续推进的半成品。还有一个极其实用的小技巧让语言模型反过来给你讲“反例空间”。比如你问“为了让这个定理成立哪些假设条件不可或缺去掉会怎么样”它可以帮你搜索那些危险边界。很多时候数学发现就是从一个反例开始的——一个边界情况被找到接下来就是调整定义让它自动覆盖这个情况。语言模型可能无法在无人引导下找到反例但在一对一对话中完成这个任务是很靠谱的。4. 常见误区与实操避坑指南4.1 把大模型输出当成可被引用的文献这是我见过最多的错误。很多学生用AI辅助做数学作业AI给出一个看起来严丝合缝的证明学生抄下来直接提交结果被老师标红。原因很简单大语言模型输出的定理证明本质上是对“文字序列的合理延续”而不是对“逻辑因果链的必然推演”。它知道“一个证明应该长什么样”并按照这个模板生成内容但不代表生成的内容经得起推敲。我建议在使用AI辅助数学时建立一条铁律任何AI生成的推导如果没有你自己独立重推一遍就不要作为任何成果的依据。把AI的输出当作“方向提示”是聪明的做法当作“权威答案”是危险的做法。这个原则用久了会形成肌肉记忆。4.2 把数值验证当成“证明过了”另一个高频错误是把数值实验当作证明。比如你用Python在百万个随机点上验证某个不等式都成立于是得出结论“这个不等式应该是真的”——这在探索阶段非常合理但它不是证明。证明是“对所有可能的情况做逻辑覆盖”数值实验只是抽样样本再多也不能覆盖无穷情况。更隐蔽的问题是数值实验本身可能带系统偏见。你生成测试样本的分布很可能不是你真正关心的那个数学集合的分布。比如你想验证某个性质在“所有凸多边形”上成立但你测试时随机生成的多边形大概率都是圆胖型的细长型几乎没有。这样即使跑了几十万个例子也不能给你想要的高置信度。做数值实验之前必须先拷问自己样本采样是否覆盖了我想宣布结论的全体4.3 形式化的成本被严重低估形式化验证是保证数学可靠性极佳的手段但它是有成本的。写一段Lean证明的时间通常是用纸笔证明同样内容的5到10倍。我把一个中等难度的引理放进Lean花了三个晚上得到的只是一个几百行的证明脚本而同行用纸笔可能一小时就搞定了。因此形式化适合的高价值场景是核心定理、重要论文的关键引理、以及任何人都能反复调用的基础库而不是所有探索性步骤。判断一个项目是否需要形式化我的标准是这个定理如果错了会让多少后续结果跟着错如果是核心地基值得投入如果只是一条不太重要的辅助引理用传统方式审阅一遍就够了。别让形式化变成新的拖延借口。4.4 过于依赖AI会导致“问题感”退化最后这条可能是最容易被忽视的。Daniel Litt在文章里写了一句话让我印象很深刻大意是“一旦什么问题都能被回答提问的质量就变成唯一稀缺的资源”。数学研究的原动力来自对问题重要性的判断——为什么这个问题值得研究、这个问题背后有什么更广泛的现象、它的答案会对哪些领域产生影响。这个判断力不是靠AI做解题训练得来的而是靠大量阅读文献、和同行对话、反复咀嚼经典论证形成的。如果研究者把精力全部花在“怎么让AI输出一个更漂亮的证明”上他的问题感会慢慢钝化最后变成只会验收机器答案的质检员。我见过几位刚入门的师弟师妹过度依赖工具之后明显对“什么问题是好问题”的判断越来越弱。这不是工具的问题而是使用方式的问题。工具负责效率和执行人负责品味和方向两者缺一不可。5. 实操过程中积累的几个独家经验讲点文档里不会写的东西。我实际用了大半年AI辅助数学研究有几个非常具体的感受。第一个是关于“提问方式”的很多人和语言模型交流时把问题描述得含含糊糊得到的回答自然也是含含糊糊他们把锅甩给AI效率低。实际上把问题精确化的过程本身就是一种数学练习你描述得越精确模型给出的路线就越具体。我后来摸索出的方法是先让模型问自己三个跟进问题再让我回答之后再让它给出解决方案。这样一轮下来模型的答案质量会大幅提升——因为它获得了足够的上下文。第二个是关于“ChatGPT式证明”的鉴别。这类证明有一个明显的特征每个局部步骤看起来都合理整体逻辑链一检查就发现中间有空档或者作者偷换了一个引理的条件。我刚开始用的时候被坑过几次后来养成一个习惯凡是AI生成的证明先找“它都没有给出定义的地方”——如果一个术语在结论中反复出现但整个证明里没有严格引入定义这个证明大概率是幻觉。严格证明的特点正是所有关键术语都有清晰的定义和约束这个特征可以被当作一个快速的验伪器。第三个好用小技巧让AI扮演审稿人。每完成一个数学推导我会把初稿丢给它要求它“以一个严厉的审稿人身份找出所有可能不严格的地方并逐条列出”。这个方法虽然不能完全替代真人审稿但非常管用。它对逻辑漏洞、定义模糊、条件缺失的嗅觉出奇地灵敏经常能找到我自己看不出来的问题。而且是免费且即时反馈的比发邮件等同行评审高效太多。第四个细节是关于记录。AI辅助研究的节奏很快一个想法出来你马上可以让它验证、扩展、找反例一天能推进好多个分支。如果不注意记录一周后你会完全忘掉自己想过什么。我现在用一个小仓库管理所有研究笔记每个条目包含问题描述、AI输出的初始结果、我自己的批注和验证状态。这个习惯让我几个月前的一个被否掉的思路在新的工具条件下成功翻案。记录被排除的错误路线和记录成功的路线同样重要。最后一个经验是关于时间和精力的分配。我的建议是给AI工具的投入设一个上限每天不超过两小时用于和模型对话或写形式化脚本剩下的大块时间留给读文献和手工推演。原因很简单AI能给你很多正确的小结果但它很难给你一个深刻的框架。深度思考需要长时间的专注和缓慢的发酵这类工作是AI替换不了的也不能因为AI工具好使就把所有时间都填进去。工具始终是工具真正的研究还得靠一颗清醒的头脑。Daniel Litt所描述的那个方向我越来越认为是真实走向数学家的核心技能会从“我能证明它”慢慢转向“我知道它为什么重要”“我知道它长什么样子”“我能把它讲给机器和别人听”。这套技能体系听起来更软实际上对数学品味的要求更高。未来能走多远的不是会操作最多工具的人而是能在工具的辅助下提出最深问题的人。