★ FEATURED ARTICLE 1. 为什么数学定理证明成了AI最难啃的硬骨头1.1 自然语言数学题与形式化证明之间隔着一条鸿沟这几年大语言模型在数学竞赛题上的表现大家有目共睹——从解IMO几何题到GSM8K应用题模型拿分越来越稳甚至能给出让人类选手都眼前一亮的解法。但如果你把这些模型丢到形式化定理证明面前它们会瞬间变成“小学生”不是因为不会算而是因为形式化证明压根不是“算出答案”这么简单。传统AI解数学题本质是生成一串自然语言的推理链只要结论正确、过程勉强讲得通就能得分。但用Lean这类交互式定理证明器做证明时机器会逐行校验你的每个推导步骤哪怕错一个符号、少一个条件、多一个隐式参数整个证明都被判无效。换句话说自然语言数学题的评分是“采分点制”而形式化证明是“零容忍制”。Numina-Lean-Agent这个项目想做的恰恰是在这道鸿沟上架一座桥。它的目标不是发明新的数学而是把一个数学定理的证明过程拆成机器可验证的小步骤然后让大模型去生成这些步骤、让Lean去检查这些步骤、再让Agent把被拒绝的步骤捡回来重试。整个循环跑通之后你会发现原本需要数学家花大量时间打磨的机械性证明工作可以大幅压缩。1.2 Lean把数学写进可执行的程序里要理解这个项目得先明白Lean是什么。简单说Lean是一个交互式定理证明器它把数学命题当作“类型”把证明当作“构造出这个类型的对象”。比如要证明“如果x是偶数那么x的平方是偶数”在Lean里就是构造一个从“x是偶数”这个命题类型到“x的平方是偶数”这个命题类型的对象。这听起来很抽象但你可以把它想象成编程Lean是一个编译器数学定理是接口证明是接口的实现。编译器只关心实现是否满足类型约束不关心实现是否“优雅”。正因为这种机械化的验证方式Lean社区攒下了庞大的mathlib库——里面已经有几十万个经过验证的定理从基础代数到分析拓扑全部可以像积木一样复用。1.3 “简化证明流程”而不是“替代数学家”标题里的“简化”两个字非常关键。我之前见过不少朋友第一次接触这类项目时会问是不是以后数学家不用干活了让AI自己证明庞加莱猜想就行这显然是想多了。目前的Agent系统包括Numina-Lean-Agent在内能处理的主要是中等复杂度的证明任务——它们擅长的是在给定目标状态下选择合适的tactic、找到需要的mathlib引理、完成局部重写这类操作。真正需要创造性构造的证明比如引入一个全新的辅助对象、设计一个复杂的归纳不变量AI依然很吃力。所以项目的正确打开方式是数学家给出证明框架或关键思路Agent负责把框架拆成Lean能接受的步骤并在卡住的地方提供候选tactic。它像个非常努力但偶尔犯傻的助手而不是能独立思考的数学家。理解了这个定位后面很多东西就顺理成章了。2. Numina-Lean-Agent的架构拆解LLM、Lean与搜索策略如何协作2.1 三个核心组件各司其职整个系统可以拆成三个部分大语言模型策略网络、Lean证明环境、Agent搜索控制循环。弄清楚这三者的分工你就知道为什么这种设计能简化流程。大语言模型负责出主意。它把自己的训练集中学过的数学证明模式映射成当前证明状态下的候选tactic。这里用的模型不是通用ChatGPT而是经过数学语料、证明语料甚至Lean代码微调的专用模型比如Llemma、DeepSeek-Prover这一路线。通用模型面对Lean状态时经常生成格式正确但语义毫无意义的tactic专用模型在这方面的表现会好几个档次。Lean证明环境负责当裁判。它接收模型生成的tactic尝试执行然后返回两种结果之一要么证明进度前进了要么报错。这个裁判严格、无情、不讲情面——也正是这种严格性让整个系统不会在幻觉上越走越远。Agent搜索控制循环负责兜底。单个tactic生成了、被拒绝了不代表证明失败。Agent会维护一棵搜索树每个节点是证明状态每条边是tactic及其结果。当一条路走不通时Agent回退到上游状态换一个tactic再试。2.2 循环反馈把“试错”变成“迭代”这套架构最核心的机制是反馈闭环。我做个类比你在写程序时IDE里红波浪线告诉你这里编译不过你改一行波浪线消失再报新的错再改。Agent在Lean里做的事情一模一样。大模型先生的不是一个完整证明而是一步。Lean执行这一步后返回新的proof state要么显示“还剩两个目标”要么显示“子目标现在是n0n”。模型看到这个状态再生成下一步。这种逐步交互极大地降低了对模型单次推理能力的依赖——模型不需要一次性想通整个证明只需要想办法把状态往前推一点。从工程角度这也让问题变得可控。一个长达几十步的证明被拆成几十次独立的“状态→tactic→新状态”循环每次都是一次小规模推理。即使中间某一步错了回退重试的成本也远低于从头再来。2.3 和同类系统的横向对比现在做Lean证明自动化的项目并不少不同系统的差异主要在搜索策略和模型分工上系统策略模型搜索方式特点GPT-f自监督预训练模型best-first search早期探索者验证了LLMtactic生成可行AlphaProof强化学习形式化环境类似AlphaZero的搜索奥数金牌级表现但资源消耗极大Numina-Lean-Agent数学微调的LLM可配置搜索策略默认beam search流程简化模块解耦容易复现Numina-Lean-Agent给我的感觉是“接地气”——不像AlphaProof那样动辄需要万卡级别算力它更强调用工程手段把现有开源模型的能力榨干净。它的设计逻辑是模型能生成80%对的部分搜索帮你弥补剩下20%人工审核兜底。2.4 为什么Agent层不可或缺有人可能会问既然有LLM生成tactic让Lean验证那不就已经是一个循环了吗为什么还需要Agent这层答案在于“策略的选择和记忆”。裸的LLMLean循环遇到失败时只能随机换一个tactic完全没有记忆也不会规划下一步动作。Agent层可以记录哪些路径已经试过、哪些tactic类型在这一类状态上成功率更高、当前深度还剩下多少探索预算。更重要的是Agent可以选择暂时搁置一个复杂子目标先去做另一个更简单的子目标——这种全局调度是纯单步交互做不到的。换句话说Agent把“生成tactic”这种低层次能力升级成了“管理证明过程”这种高层次能力。这也是题目里“简化数学定理证明流程”的真正含义——不是让每一步更聪明而是让整个流程更有章法。3. 从目标到QED一个证明任务的完整交互链路3.1 先看一个最小的例子为了让你直观感受这套流程我拿一个非常初等的定理来演示对任意自然数n0 n n。这个例子简单到几乎不需要证明但它能完整展示Agent、LLM和Lean三者之间的对话模式。在Lean里这个定理可以写成theorem zero_add (n : ℕ) : 0 n n : by induction n with | zero simp | succ n ih simpa [Nat.succ_eq_add_one] using ih这段代码里by之后的内容就是证明脚本。induction n对n做归纳zero分支用simp搞定succ分支用ih归纳假设加上simp收尾。人类看这个脚本觉得平平无奇但Agent在证明过程中经历的东西要琐碎得多。3.2 Agent视角下的逐步决策当Agent拿到∀ n, 0 n n这个目标时它看到的是Lean返回的原始proof state⊢ ∀ (n : ℕ), 0 n n模型第一件事是决定要不要用intro把这个全称量词变成条件句。这一步成功率极高因为几乎所有的全称命题第一步都是引入变量。LLM生成intro nLean接受状态变成n : ℕ ⊢ 0 n n到了这一步模型面临决策点是直接simp还是做归纳经验不足的模型可能直接生成simpLean执行后确实能关闭目标——但如果把0换成更复杂的表达式直接simp往往不够。好的策略模型会在这一步选择induction n因为它知道0 n这类命题需要对n做结构归纳。阶段LLM生成的tacticLean返回的新状态搜索树变化初始—⊢ ∀ n, 0 n n根节点第1步intro nn : ℕ ⊢ 0 n n深度1第2步induction n两个子目标分叉出现两个子节点第3步case zero simp子目标1关闭剪枝一个分支第4步case succ simpa [...] using ih子目标2关闭全部关闭得到QED这张表看起来理性清晰但真实运行中远不是直线下来的。模型有可能在第3步生成一个错误的tactic比如把simp写成simp [add_zero]而add_zero根本未被引入Lean直接报错。这时Agent会把这个节点标记为失败然后回到第2步生成的另一个子目标先处理而不是死磕这个失败的叶子。搜索策略就在这种“前进—受阻—绕行”的节奏中推进。3.3 漫长的证明如何保持“不迷路”像0 n n这种一步到位的证明体现不出Agent的价值。真正能体现价值的是那种需要二十步、三十步的证明——比如证明某个数列极限的性质或者某个代数结构的唯一性。这种长证明最大的敌人是上下文爆炸。每走一步Lean的proof state都会变大变量增多、假设变多、目标变复杂。LLM的上下文窗口是有限的当状态累积到一定程度时模型会“忘了”最开始的目标是什么开始生成与主线无关的tactic。Numina-Lean-Agent的做法是通过Agent层控制“观察半径”——不是把所有状态一股脑塞给模型而是筛选出当前子目标相关的变量和假设剔除无关内容。这就像登山时你不必盯着整座山只需要看清眼前十米的路。每次只关注局部状态反而比追求全局视野更有效。3.4 每一步都对不代表最终能证明还有一个新手容易误解的地方AI生成的每一步都通过了Lean验证为什么最终还可能是失败的证明原因是“目标分裂”。一个看似无害的tactic可能把目标拆成三个子目标其中两个很容易第三个却极其复杂。搜索树沿着这两个容易的子目标狂飙最后在第三个子目标上发现根本推不动这时之前的进展全部作废——因为Lean要求所有子目标都被证明一条支线失败整个证明失败。这也是为什么Agent需要全局的“难度评估”。成熟的实现会在每一步推进后评估剩余子目标的总量和不变量程度如果发现某个支线进入了复杂区域会主动回退而不是贪图眼前的小胜利。这种策略很像下棋时的局部战斗与全局弃子——为了整体的可解性必须牺牲看起来有用的步骤。4. “简化”不等于“全自动”关键场景、能力边界与适用人群4.1 哪些证明任务最适合交给它说了半天架构和流程落到实际问题这个东西到底能帮你证明什么根据我观察到的实际案例第一类非常适合的任务是“代数机械化操作”。比如化简一个复杂的多项式等式、对某个求和公式做归纳证明、用已有引理做重写。这类证明特征明显路径固定、每一步选择不多、主要靠细心。大模型对这类任务几乎不会走错路。第二类任务是“已有mathlib引理的查找与拼接”。当你的目标恰好是某个已知引理的特例时Agent可以通过语义匹配找到exact或rw就能完成证明。这其实是大模型最擅长的模式匹配能力在起作用。第三类是“中等长度的构造性证明”。比如证明某个映射是单射、某个集合是可数的——这类证明往往需要几步关键构造加几次化简不会出现过于精巧的思路但步骤多、容易在细节上卡壳。Agent的作用就是把这些细节填平。你可以把这三类任务的共同点概括成一句话证明的主干思路是明确的只是具体执行繁琐。Agent最适合的就是这种“有方向但怕麻烦”的工作。4.2 哪些场景会让它当场翻车反过来看有四类场景目前依然是无解的。第一需要新定义的证明。比如证明过程中需要引入一个前人没定义过的辅助对象——一个序列、一个映射、一个代数结构。模型很难凭空创造定义因为它的训练集中没有这种“新东西”的先例。第二需要复杂归纳不变量。真实数学证明里归纳时需要构造一个比目标本身更强、更精心的命题。这种“加强归纳假设”的创意是当前模型最大的死穴。第三需要跨章节知识融合。目标看起来只涉及代数但证明的核心步骤需要用到一个深度分析定理。模型在面对纯代数状态时不会主动想起分析工具因为相关性检索就过不了关。第四超长证明链。一百步以上的证明即使每一步都对搜索树的膨胀也会让计算成本爆炸。Agent的搜索策略只能缓解无法根除。4.3 隐藏成本算力、时间与人工审核我必须提醒你用Agent做定理证明不是免费的。即使是中等规模的证明本地跑一个微调模型推理单步tactic生成可能只要几百毫秒但一次搜索要探索几百个节点累计起来就是几分钟到几十分钟。如果使用API调用方式成本更是肉眼可见。更被低估的是人工审核成本。Agent给出一个QED标记时并不意味着证明一定有价值——它只是说“每一步都通过了Lean验证”。你要检查这个证明是否绕了远路、是否依赖了某些不自然的假设、是否对代码后续维护友好。我见过Agent用25步完成一个人类用5步就能写完的证明逻辑上没错但数学上毫无美感。所以我把这个工具定位成“加速器”而不是“替代品”。它加速的是你从“思路清晰”到“证明完成”之间的距离而不是从“问题提出”到“思路产生”的距离。4.4 谁最适合使用这套方案从我的经验看以下三类人最值得投入时间研究Numina-Lean-Agent组数学家如果你正在做Lean形式化写作比如加入mathlib贡献Agent能帮你快速处理引理证明中的琐碎分支让你把精力集中在需要灵感的环节。第二类是机器学习研究者这个项目本身就是很好的研究对象——它的数据管线、tactic采样策略、搜索回退机制都是可以复用到其他推理类任务上的方法论。第三类是软件验证工程师虽然Lean主要面向数学但它的底层类型论和Coq、Agda同源。你在Lean Agent上学到的“把规范拆成可验证子目标”的思路完全可以迁移到程序验证领域。不太适合的是对两者都没兴趣的普通用户——如果你既不想学Lean也不关心AI推理机制那这个工具目前对你的实际帮助有限。5. 实操踩坑记录错误tactic、死循环与上下文耗尽5.1 看起来对但Lean就是不肯放行我第一次跑通完整流程后最大的感触是大模型生成tactic的错误模式和“笨学生”的错误模式惊人地相似。最常见的错误是缺少必要的简化引理。模型会生成simp [foo]但当前上下文中foo根本不是一个可用的定理名Lean直接抛unknown constant。这种错误不是语法问题而是模型的“知识幻觉”——它从训练集里记住了这个引理存在但没记住它需要在什么状态下引入。第二种常见错误是重写方向搞反。模型会用rw [← h]但实际需要的是rw [h]。这种错误单看每一步完全合理尤其是当模型没注意到当前目标是a b还是b a时。第三种错误更隐蔽使用了正确的tactic但作用位置不对。比如对n做了cases n但应该对n m做分析或者用了induction h但h是个命题而不是变量。面对这些错误我总结的排查顺序是先确认当前proof state和模型看到的状态一致再看tactic引用的引理名称是否在当前作用域内最后检查重写方向。Agent会自动重试但如果你要人工介入按这个顺序定位会快很多。5.2 搜索死循环看似在努力实际在原地打转第二个让我头疼的坑是死循环。Agent会陷入一种“生成tactic→Lean说失败→回退→再生成几乎相同的tactic→再失败”的循环中尤其当温度参数设置过高时模型会在同一个状态附近反复试探消耗大量预算却毫无进展。我的解法是给搜索加上两个限制。第一限制同一状态上的尝试次数比如一个节点最多生成5个不同的tactic第二监控状态哈希序列发现状态重复或回退频繁时主动降低探索温度或强制切换到另一个分支。从根因上讲这是一个“动态探索与利用平衡”的问题。搜索前期希望模型多探索不同路径所以温度调高搜索后期需要模型在已有路径上精耕细作所以温度调低。我在项目里实现的是按深度线性衰减的温度调度效果比固定温度好不少。5.3 上下文窗口被撑爆状态太长也是病第三个坑来自Lean的状态本身。一个真实项目中期的proof state可能会包含几十个变量、几十条假设序列化后轻松超过几千token。如果把完整状态直接填给LLM上下文窗口很快就会报警而且模型收到的“噪音”远大于“信号”。我试过几种缓解方案。最粗暴的是截断——只保留最近修改过的变量和假设稍微优雅一点的是按名称前缀过滤去掉不相干的命名空间再进阶一点的是手动标注关键假设告诉Agent哪些是核心、哪些可以忽略。但最有效的还是结构拆分。如果一个proof state已经复杂到无法塞进上下文说明这个子目标本身就太大了需要人工介入拆分。Agent不是万能的它适合处理的是“状态足够小、步骤足够清晰”的证明节点。5.4 环境版本问题同一段代码换个环境就“翻车”最后聊一个没有技术含量但特别折磨人的坑环境版本不一致。Lean社区迭代很快Lean 3时代的语法和Lean 4已经有很大差异而mathlib更是几乎每天都在更新。同一个simp调用在旧版本mathlib里引理集不同行为可能完全不同。如果你是在公共代码库上跑实验我的建议是固定Lean版本、固定mathlib版本、锁定elan工具链。不要图方便用“最新版”宁可牺牲一点性能也要保证复现性。另外如果在跑Agent时遇到诡异报错先检查Lean环境的lean-toolchain文件看看当前项目锁定的是哪个版本再去mathlib仓库查对应版本的引理状态。这个动作能帮你排除掉一半的“Agent问题”。6. 落地方案怎么把它装进你的工作流6.1 环境准备与项目初始化如果你看完前面这些内容还想试试那我给你一套能跑通的最简方案。首先准备Lean环境。我推荐用elan作为版本管理器安装命令很简单curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh elan install leanprover/lean4:stable然后初始化一个Lean项目注意要带mathlib支持lake new demo_agent math cd demo_agent lake build如果你的网络环境不支持直接拉取mathlib缓存可能会等很长时间——这是正常的耐心等一次后面就会好很多。另外VS Code装好Lean 4扩展这样你能看到每个证明步骤的实时状态调试Agent推理时非常有帮助。6.2 模型选择与Agent配置模型方面我建议从已经开源、且在Lean语料上微调过的模型入手这类模型对tactic生成的理解比通用模型强太多。如果你本地GPU显存不够可以选择API调用方式但要注意延迟和成本。Agent配置上最关键的几个参数尝试次数每个状态最多尝试生成几个tactic我一般设在5~8之间。探索宽度并行保留的搜索路径数量建议初始设为4避免搜索树过宽导致内存爆炸。温度调度初始0.7深度增加后逐步降到0.3兼顾探索与收敛。上下文裁剪开启按变量相关性过滤只保留与当前子目标直接相关的假设。几个参数之间有明显的联动关系探索宽度过大时尝试次数要相应减少否则单条路径的“深度思考”会被稀释。我踩过的坑是盲目追求宽度结果每个分支都浅尝辄止反而不如窄而深的效果好。6.3 跑一个最简单的Agent循环做测试配好环境之后不要直接挑战难题先让Agent证明一个引理来验证配置是否正常。比如拿#check一个简单的恒等式看看Agent能不能在几步内完成。我用过的最小测试是这样的让Agent证明∀ n m : ℕ, n m m n。这个定理需要归纳法和一些结合律、交换律的引理拼接步骤不超过10步但足够暴露大多数配置问题。当Agent能稳定跑通这类命题后再逐步加大难度先换成带条件的分支命题再换成涉及自定义结构的命题。每一步加难都能帮你定位瓶颈是模型能力还是搜索参数。6.4 它到底该不该进你的工具箱最后给你一个判断清单。如果你符合以下任意一条我觉得值得投入时间深入折腾你在做Lean数学形式化方向的长期研究需要高频处理琐碎的证明细节。你在研究LLM的推理增强方法想找一个可以量化验证“推理进步”的环境。你有一定的工程能力愿意花时间调搜索参数、处理版本兼容问题。如果你只是抱着“让AI帮我证明一个猜想”的预期来用它那我劝你冷静。这个工具不会给你惊喜——它不会解出你解不开的数学题但会帮你把已经想明白的证明过程写得更快、更规范。我在实际使用中最实在的体会是把它当成“形式化版本的结对编程搭档”。它帮你码代码你帮它把关方向配合得当的话效率提升是一目了然的。至于那些指望全自动证明的时代至少对我这种普通研究者来说还没来。
阅读完成 · 觉得有帮助？
