设想一所大学图书馆深夜发生了一起数学「悬案」——一份珍贵手稿的第100页被人撕走了。经验丰富的侦探老王面对满地纸屑和脚印，要回答的终极问题是：凶手到底是谁？他不能凭直觉下结论，而必须找到一条环环相扣的「证据链」：每个脚印对应什么鞋码，鞋码对应谁的行踪，行踪又是否被监控证实。数学里的定理证明，本质上就是给一个命题案件寻找这样一条无可辩驳的证据链——从已知条件出发，每一步推理都踩着公认的规则，最终抵达结论。 现在，AI研究者提出了一个大胆的设想：能不能让大语言模型（LLM）来扮演那个见多识广、直觉敏锐的「侦探顾问」，再让 Lean、Coq、Isabelle 这类形式化证明器充当铁面无私的「法官」，两者搭档去破解更多数学悬案？这篇文章就带你围观这套「AI+法官」组合的办案日常——大模型负责补全证明步骤、规划搜索路线、给出战术建议，证明器负责逐条验证每一步是否真的有据可依，两者最终配合着走通一条完整的证明之路。你不需要懂数学细节，只要带着看侦探剧的心情，就能看懂这个正在改变数学研究方式的科技前沿。

岗位关联

对 AI 从业者而言，这是理解「AI 与形式化验证如何协同」的最佳切入点：掌握 LLM 在定理证明中的定位、方法与评估口径，你就能在人机协同推理、可信 AI 工程化等方向找到自己的位置。

目录
  1. 可视化演示
  2. 定理证明基础：证据链与推理规则
  3. LLM的角色：侦探顾问的三项本事
  4. 补全证明步骤：递上战术指令卡
  5. 搜索策略：迷宫里的路线规划
  6. 证明验证：铁面法官的终极审核
  7. 评估方法：命中率怎么算
  8. 数学分支应用：不同现场的破案难度
  9. 挑战与局限：长案子的误差累积
  10. AI 应用场景
  11. Python 演示
  12. 常见误区
  13. 面试题

可视化演示

动态演示大语言模型辅助数学定理证明探的核心机制，通过概览/流程/对比/趋势四种模式展示关键概念与交互流程。

本节配有交互动效（进入视口后自动加载，约 3KB）。

大语言模型辅助数学定理证明探：LLM在 LLM在形式化证明中的角色定位 LLM与Lean/Coq/Is 核心机制可视化 大语言模型辅助数学定理证明探整体架构与关键组件

定理证明基础：证据链与推理规则

侦探老王的第一课永远是：办案不能靠脑补。数学证明同样拒绝任何「我觉得显然成立」的表述。在一个数学系统里，命题就像案情陈述，而推理规则则是侦探行业公认的取证规范——每一条新的线索，都必须由旧线索依据规范推出来，才会被法庭接纳。

形式化证明器（比如 Lean、Coq、Isabelle）就是把这些规范变成可执行的程序：用户提交任何一步推理，证明器都只问一句「你依据哪条规则？」如果答不上来，直接驳回。它们的内部维护着一棵由规则构成的「证据树」，树的根是已知公理，每一步分枝都对应着一次合法推理。最基础的一条推理规范叫「肯定前件」，它相当于侦探圈子的「铁律」：如果你已经确认「如果下雨，地面就湿」这条规则成立，又亲眼看见下雨，那么「地面湿」就是板上钉钉的事实。

所以，所谓「证明」，就是把无数个这样的小步骤首尾相接：每次只走一小步，每一步都有规则背书。侦探老王把这种工作叫作「铺证据链」——链子越长越要小心，但每一步只要合规，就不会断。

P→Q,  P⊢Q\displaystyle P \rightarrow Q,\; P \vdash Q
这条公式说的是：已知「P 推出 Q」和「P 成立」，就必然能得到「Q 成立」。它是所有数学证明中最常用的一步「证据拼接」。
  1. 条件证据$P \rightarrow Q$，读作「若 P 则 Q」，表示一条已被法庭认可的推导规则。
  2. 事实证据$P$，表示当前已经确认成立的命题，相当于侦探手里攥着的物证。
  3. 推导符$\vdash$，读作「可推出」，它连接左侧的已知证据与右侧的必然结论。
  4. 必然结论$Q$，只要前两条证据为真，$Q$ 便没有任何辩驳余地，法官必须采纳。

LLM的角色：侦探顾问的三项本事

一个优秀侦探最值钱的不是体力，而是经验带来的直觉。老王接到新案子，扫一眼现场就能报出几个可疑方向，虽然不一定对，但能大幅缩小排查范围。大语言模型在定理证明中的角色，正像这位「侦探顾问」：它读过海量数学文本和形式化证明库，对「下一步大概率可以怎么走」有统计意义上的直觉。

具体来说，LLM 要做三件事。第一，当证明在某一步卡住时，它负责补全证明步骤——直接预测下一个可行的推理动作；第二，它可以连续生成多个候选策略，让验证器逐一尝试，而不必只押一个答案；第三，它能预测证明状态的变化趋势——当前这个子目标到底离最终结论更近了，还是绕进了死胡同。这三项能力恰好对应了侦探办案时「提方向、给方案、看苗头」的本事。

但请注意，侦探顾问的直觉只是「建议」，不是「结论」。LLM 给出的候选步骤可能满嘴跑火车，只有经过法官那一关，才算真正在案件卷宗上落了笔。

s^t=arg⁡max⁡s  Pθ(s∣C,  gt)\displaystyle \hat{s}_t = \mathop{\arg\max}_s\; P_\theta(s \mid C,\; g_t)
大模型在做的事，就是根据已知的证明上下文 $C$ 和当前待证目标 $g_t$，给每一个候选步骤 $s$ 打分，然后挑出分数最高的那个，把它递给验证器去核实。
  1. 上下文$C$，表示已经完成的证明步骤和当前可用的前提条件，相当于侦探已收集在案的线索。
  2. 当前目标$g_t$，表示此刻尚未证明的子命题，也就是案件尚未揭开的那一环。
  3. 条件概率$P_\theta(s \mid C, g_t)$，模型给出「在此线索下，下一步走 $s$ 有多大的胜算」。
  4. 取最大$\mathop{\arg\max}_s$，表示从所有候选动作里挑出概率最高的那一个，交给法官验证。

补全证明步骤：递上战术指令卡

在形式化证明器里，用户很少直接写「因为 A 所以 B」这种自然语言，而是递给证明器一张张「战术指令卡」——专业术语叫 tactic。每张卡片上写着一个小动作：把目标拆开、把前提引入、应用某个已知引理……证明器执行这张卡片，把当前的证明状态转变成新的状态。你可以想象侦探每走一步，都要向法官提交一张写有「本次行动依据」的申请单。

LLM 的角色，就是帮侦探批量填写这些指令卡。一个常见的应用场景叫「填洞」：证明器在推理中留下一个空位（hole），表示「这里需要你给出中间引理或步骤」，LLM 负责把这个洞补上。它还会顺着依赖条件推：如果当前的子目标依赖某条引理，而引理本身又需要另一个前置条件，模型就一层层往前追，直到所有前提都落在已知公理上。

回看侦探老王的工作：他办案的过程何尝不是一张张指令卡？「调取监控」是一条指令，执行后卷宗里多了一条行踪记录；「比对指纹」又是一条指令，执行后嫌疑范围缩小。LLM+证明器的组合，就是把办案的「出主意」和「走流程」彻底分工了。

Γ→tacticΓ′\displaystyle \Gamma \xrightarrow{\texttt{tactic}} \Gamma'
这条式子表示：一张 tactic 指令卡把旧证明状态 $\Gamma$ 转变成了新状态 $\Gamma'$。整个证明过程，就是通过一连串这样的状态转移，最终抵达「无懈可击」的终态。
  1. 旧状态$\Gamma$，由当前已证命题和待证目标共同构成，相当于案件此刻的全部卷宗信息。
  2. 指令卡$\texttt{tactic}$，是用户或 LLM 给出的一个具体推理动作，比如 intro 或 apply。
  3. 转移箭头$\xrightarrow{\texttt{tactic}}$，表示把这张指令卡交给证明器执行后，状态发生了合法变化。
  4. 新状态$\Gamma'$，执行完成后更新的卷宗——可能目标变小了，也可能新增了前提。

搜索策略：迷宫里的路线规划

有了 tactical 指令卡，下一个问题随之而来：从一个证明状态出发，可以执行的指令卡有成千上万张，侦探该先试哪张？如果每张都试，那是一条指数爆炸的迷宫——即使证明只有几十步，可能的路径也远超宇宙原子总数。所以，聪明的侦探不会无脑乱闯，而会带着一张「路线优先级清单」进入迷宫。

这套路线规划在 AI 里叫搜索策略。目前常用的有两种：束搜索（beam search）会同时维护若干个最有希望的中间状态，像派出几个小分队分头探路；蒙特卡洛树搜索（MCTS）则会在候选路线上做随机模拟推演，把每一步「先用模拟走几遍看看胜率」，再优先展开模拟胜率高的分支。两者背后都站着一个关键角色——启发式评估函数 $h$，它用来给每个未完成状态估算「离真相还有多远」。

有了这套策略，LLM 的直觉就与搜索框架真正融合了：大模型负责提供高质量的 $h$（路线偏好），搜索算法负责保证不会漏掉真正可行的路。侦探的直觉加警方的系统排查，破案率自然水涨船高。

f(n)=g(n)+h(n)\displaystyle f(n) = g(n) + h(n)
每个候选状态 $n$ 都按「已经付出的代价」加上「估计还需要的代价」来排名，总分低的路线优先试探，这就是有计划的迷宫探索。
  1. 已花代价$g(n)$，从证明起点走到当前状态 $n$ 已经用掉的步骤数，相当于侦探已经投入的办案时长。
  2. 估计剩余$h(n)$，启发式函数对「从 $n$ 到完成证明还需多少步」的估算，像老侦探扫一眼现场给出的直觉。
  3. 合计评估$f(n)$，两者相加，值越小，说明这条路既走得快又看起来离真相近，应当优先派警力。
  4. 排序展开实际搜索时，优先选取 $f(n)$ 最小的节点展开，失败就回退换路，形成「探索—碰壁—回溯—再探索」的节奏。

证明验证：铁面法官的终极审核

搜索找到了一个看起来像模像样的证据链，数学证明就算完成了吗？远远没有。在自然语言论文里，审稿人可能因为「此处显然」四个字就放过你，但形式化证明器这位法官绝不会通融。它要的不是「看起来合理」，而是每一步都必须可以机械地检查——这背后靠的是类型论。

类型论把每个数学命题看成一种「类型」，把命题的证明看成构造出这个类型的一个「实例」。这是什么意思？打个比方：命题「存在一个犯罪现场的目击证人」是一种类型，那么提供一份带签名的证人证词，就是构造了一个实例。库里-霍华德对应告诉我们：证明即程序，一个类型检查器就是一台终极验证机。Lean 等证明器本质上都是类型检查器，它们读入你在证明中构造的程序（即证据链），逐行检查类型是否匹配。

所以在整个系统里，LLM 生成的证明草稿只是「证据包」的毛坯，只有类型检查器逐项核验通过，法官才会盖下「证据链合法」的红章。侦探可以天马行空，但法官只认死理——这也是形式化证明最迷人的地方：一旦通过验证，就绝对不可能有漏洞。

e:A×B  ⟺  π1(e):A  ∧  π2(e):B\displaystyle e : A \times B \;\Longleftrightarrow\; \pi_1(e) : A \;\wedge\; \pi_2(e) : B
这条式子说明了「合取命题的证明」如何被构造：一个同时证明 $A$ 和 $B$ 的证明，本质上是一个有序对，左半部分证明 $A$，右半部分证明 $B$。
  1. 合取类型$A \times B$，表示命题「$A$ 且 $B$」对应的类型，它要求两部分证据同时在场。
  2. 证明实例$e : A \times B$，表示 $e$ 是一个同时给出 $A$ 与 $B$ 证明的证据包，如同一个写有双重结论的卷宗。
  3. 左分量$\pi_1(e)$，取证据包的第一部分，它必须是命题 $A$ 的合法证明。
  4. 右分量$\pi_2(e)$，取第二部分，它必须是命题 $B$ 的合法证明。

评估方法：命中率怎么算

现在问题来了：各路研究者都在用 LLM 做定理证明，怎么比较哪个模型更好用？一个人可能说了十次思路，正中靶心的只有一次；但他要是能说一千次呢？这里需要一把科学的尺子。评估 LLM 定理证明能力最常用的指标叫 pass@k——它衡量的是：给模型 $k$ 次尝试机会，至少有一次成功证明的概率。

这个指标非常像侦探考试：考官把一个积案丢给你，允许你提交 $k$ 份侦查方案，只要有一份方案最终被法官采信，你就算过了这关。显然，$k$ 越大，过关率越高。为了剔除抽样误差，研究者会把模型在同一个题目上重复生成 $n$ 次，统计其中成功次数 $c$，再按组合数学算出一致无偏的估计值。

当然，pass@k 不是唯一的尺子。研究者还会统计整体成功率、对比人类数学家写出的证明长度和可读性。毕竟，侦探的价值不只是「最终破案」，还包括「少走弯路、让同行听得懂推理过程」。

pass@k=1−(n−ck)(nk)\displaystyle \text{pass@k} = 1 - \frac{\binom{n-c}{k}}{\binom{n}{k}}
简单说：从 $n$ 次生成中选 $k$ 次，全部选到失败样本的「倒霉概率」是 $\binom{n-c}{k}/\binom{n}{k}$，pass@k 就是它的反面——至少选中一次成功样本的概率。
  1. 总生成数$n$，模型在同一个证明任务上被要求生成的候选方案总数。
  2. 成功数$c$，其中通过验证器检查的方案个数，即真正走到真相的方案。
  3. 失败组合$\binom{n-c}{k}$，从失败方案里任选 $k$ 个，导致全盘皆输的选法数量。
  4. 总数组合$\binom{n}{k}$，从全部方案里任选 $k$ 个的总选法数量。
  5. 取补$1 - \frac{\binom{n-c}{k}}{\binom{n}{k}}$，用 1 减去「全军覆没」的概率，就得到「至少一次成功」的命中率。

数学分支应用：不同现场的破案难度

不是所有的数学悬案都适合让「AI 侦探+法官」组合出动。老王最清楚：同样是案子，盗窃案往往证据链清晰，而高智商犯罪可能连案发现场都难以定义。数学的各分支恰恰有这种「破案难度」差异。

目前最成熟的领域是代数与数论。原因很直白：这些分支拥有大量结构规整、机械化程度高的证明范式，形式化数学库（如 Lean 的 Mathlib）里积累了海量现成证明，LLM 有充足的「卷宗」可学，补全证明步骤的成功率相当可观。相比之下，分析与几何就麻烦得多——涉及极限、连续性、拓扑这类抽象概念时，自然语言数学里的「显然」在形式化系统里往往要用几十步专门操作来刻画，证据链既长又脆。组合学与逻辑学的处境则介于两者之间：组合题目的搜索空间常常爆炸，逻辑题目又往往需要精巧的构造式思维，目前仍在探索阶段。

读懂这张「难度地图」很有价值：如果你是一个想动手实践的工程师，可以先从代数与数论分支找练手案例；如果你研究的是分析难题，则要清醒地认识到，那条证据链很可能比想象中长得多。

p^B=1NB∑i=1NB1[provedi]\displaystyle \hat{p}_{\mathcal{B}} = \frac{1}{N_{\mathcal{B}}} \sum_{i=1}^{N_{\mathcal{B}}} \mathbb{1}[\text{proved}_i]
这是对某个数学分支 $\mathcal{B}$ 估计「破案成功率」的公式：把所有尝试过的题目里被成功证明的比例算出来，作为该分支当前难度的晴雨表。
  1. 分支集合$\mathcal{B}$，指定一个数学领域，例如代数、几何或组合学。
  2. 题目总数$N_{\mathcal{B}}$，在该领域上尝试证明的题目数量，相当于受理的案件数。
  3. 成功指示$\mathbb{1}[\text{proved}_i]$，当第 $i$ 个题目最终被证明器验证通过时取 1，否则取 0。
  4. 平均$\sum_{i=1}^{N_{\mathcal{B}}} \mathbb{1}[\text{proved}_i] / N_{\mathcal{B}}$，把成功的题目数归一化，得到该分支的经验成功率。

挑战与局限：长案子的误差累积

侦探老王最怕什么？不是单步判断失误，而是一桩需要几十个环节环环相扣的长案子——只要中间某一步的直觉稍微偏了一点，整条链就会在终点垮掉。LLM 辅助定理证明的当前最大瓶颈，正是这种「长链条推理」的误差累积。

假设大模型每一步给出正确策略的概率高达 95%，表面看起来相当可靠。但如果一个证明需要 20 步，整体成功率就要把每一步的概率连乘起来：0.95 的 20 次方只有约 36%。更糟糕的是，数学语料天然稀疏——人类历史上的严格证明远没有互联网上的自然语言多，模型学到的高质量「推理对话」就更加稀缺。这导致 LLM 经常在短证明上表现出色，一遇到长证明就原形毕露：头几步气势如虹，越到后面越像没有目击者的深夜街道。

所以，现阶段最务实的路线不是让 AI 独立破长案，而是「人机协同」：数学家负责把握全局方向，把大目标分解成一个个小引理，LLM 负责攻克每个小引理的中间步骤，证明器在每一步严格把关。侦探的直觉、顾问的建议、法官的审核，三者各司其职，才能把这个领域真正推向更远的数学边界。

Pall=∏i=1npi\displaystyle P_{\text{all}} = \prod_{i=1}^{n} p_i
这条公式揭示了长链的残酷之处：一个含 $n$ 步的证明要做到每一步都对，整体成功率就是每一步成功率的连乘积。步骤越多，风险越像滚雪球一样膨胀。
  1. 单步成功率$p_i$，第 $i$ 步推理在验证器那里通过的概率，可以理解为每段线索被法庭采信的概率。
  2. 连乘符号$\prod_{i=1}^{n}$，把从第 1 步到第 $n$ 步的所有概率逐个相乘。
  3. 整体成功率$P_{\text{all}}$，整条证据链完整成立的概率，它随 $n$ 增大而指数级衰减。

AI 应用场景

开源数学库的自动补全

阶段：数据生产与标注辅助

解决的问题：Lean 的 Mathlib 等大型形式化数学库拥有数万条「未完成的证明洞」，人工逐个补全极其耗时。传统的做法是数学家用编辑器手动搜索引理、手动填写 tactic，效率低下且门槛高。LLM 可以针对当前证明状态自动生成候选 tactic 和中间引理名，维护者只需对证明器的验证结果做最终确认。

具体案例：维护者在 Mathlib 的 pull request 中留下一个 sorry（表示此处证明暂缺），接入 LLM 插件的 IDE 立刻基于当前上下文推荐三步以内的补全方案，并把每一步放进 Lean 验证器里跑一遍，通过后自动填充，让 PR 的合并周期从一周缩短到一天。

智能合约与硬件验证

阶段：AI 生成 + 外部验证闭环

解决的问题：传统软件验证要求工程师手写大量「规范证明」，证明合约没有任何路径可达错误状态，成本极高。LLM 可以先分析智能合约的代码语义，生成「该函数不会溢出」「该状态转换不会破坏不变量」等候选证明结构，再由 Coq 等验证器逐条检验，把工程师从繁琐的底层证明细节中解放出来。

具体案例：一家区块链安全公司在审计 DeFi 合约时，把 200 个待验证的安全性命题交给「LLM+验证器」流水线：LLM 生成候选证明脚本，验证器批量执行并给出反例，模型根据反例反馈迭代修正，最终将人工审计的工作量压缩了 60% 以上。

数学研究助手

阶段：研究探索与假设生成

解决的问题：数学家在尝试证明一个新猜想时，往往要在多条可能的证明路线间徘徊。传统方式靠个人经验试错，一个方向可能耗费数周才发现走不通。LLM 可以在形式化系统内同时生成多条证明路径的雏形，配合搜索策略快速判断哪条路线可行、哪个中间引理是瓶颈。

具体案例：组合数学团队在探索一类新的图论不等式时，使用「LLM 推荐引理 + Isabelle 快速验证 + MCTS 路线回溯」的框架，让 AI 先淘汰掉 80% 的错误路线，研究者集中精力在剩下的两三条候选路线上手工推进，最终将新定理的证明周期从半年缩短到两个月。

Python 演示

python84 行
# -*- coding: utf-8 -*-"""最小演示：LLM 提供 tactic 建议 + 法官验证器把关的证明搜索流程"""import heapqimport random  class ProofState:    """一个证明状态 = 当前目标 + 已有前提 + 走过的步骤"""     def __init__(self, goal, context=(), path=()):        self.goal = goal        self.context = list(context)        self.path = list(path)     def is_proved(self):        """当目标已经出现在前提中（或直接为 True）时，证明完成"""        return self.goal == "True" or self.goal in self.context     def clone(self, goal, step, new_context=None):        ctx = new_context if new_context is not None else self.context        return ProofState(goal, ctx, self.path + [step])  class TacticAgent:    """模拟 LLM：针对当前目标随机推荐候选 tactic，体现'出主意'"""     def __init__(self):        self.tactics = ["intro", "exact"]     def suggest(self, state):        random.shuffle(self.tactics)        return self.tactics[:2]  class Verifier:    """铁面法官：逐条检查 tactic 是否合法，合法才返回新状态"""     def __init__(self, agent):        self.agent = agent     def step(self, state, tactic):        if tactic == "intro" and state.goal == "a -> a":            # 引入前提 a，目标从 a->a 缩小为 a            return state.clone("a", tactic, state.context + ["a"])        if tactic == "exact" and state.goal in state.context:            # 目标已在前提中，直接用 exact 收尾            return state.clone("True", tactic)        return None  class Prover:    """best-first 搜索器：按路径长度排序，优先试探短路径"""     def __init__(self, verifier):        self.verifier = verifier        self.visited_count = 0     def prove(self, start, max_steps=50):        heap = [(0, start)]        while heap:            _, state = heapq.heappop(heap)            self.visited_count += 1            if self.visited_count > max_steps:                return None            if state.is_proved():                return state.path            for tactic in self.verifier.agent.suggest(state):                new_state = self.verifier.step(state, tactic)                if new_state is not None:                    heapq.heappush(heap, (len(new_state.path), new_state))        return None  if __name__ == "__main__":    agent = TacticAgent()    verifier = Verifier(agent)    prover = Prover(verifier)    start = ProofState(goal="a -> a", context=["a"])    found = prover.prove(start)    if found:        print("证明成功，路径:", " -> ".join(found))    else:        print("当前条件下没有找到证明路径")    print("访问状态数:", prover.visited_count)
目的：这段代码演示了「LLM 建议者 + 验证器 + 搜索器」的完整协作闭环——用 intro 和 exact 两张指令卡，在极简的命题逻辑库里搜索出一条从目标到证明完成的路径。
  1. class ProofState把证明状态建模成「目标 + 前提 + 历史路径」，对应侦探手里不断更新的卷宗。
  2. def is_proved目标出现在前提里就等于真相大白，这是搜索终止的判定条件。
  3. class TacticAgent模拟 LLM 的「提建议」能力，每次给出少量候选 tactic。
  4. Verifier.step法官逐条检查建议，只有完全合法才返回新状态，非法建议直接丢弃。
  5. if tactic == "intro"处理「引入前提」指令：目标 a -> a 缩小为 a，前提表里多了一个 a。
  6. if tactic == "exact"处理「命中前提」指令：目标已经握在手里，直接宣布该分支证明完成。
  7. heapq.heappush(heap, (len(new_state.path), new_state))路径越短优先级越高，这就是一种最简单的启发式排序。

常见误区

误区「大模型输出了一大段像模像样的数学推导，每一步看起来都严谨，这肯定就是正确证明了，直接用就行。」

正解LLM 是侦探顾问，不是法官。它的证明文本基于统计规律拼凑，可能看起来通顺，却在某个隐蔽处偷换了逻辑前提。形式化证明器的存在正是为了打破这种错觉——只有逐条经过类型检查、被证明器判为合法的证据链，才算真正的证明。把 LLM 的输出直接当作成品，等于是让嫌疑人自己给自己开无罪证明。

为何常见：大模型在自然语言对话中表现太流畅，人很容易把「说得头头是道」和「经得起检验」混为一谈，忽略了生成式模型本质上是在做概率预测，而不是逻辑推演。

误区「Lean、Coq 这些工具不就是帮人做数值计算的吗？数学定理的证明归根到底还是要靠人的创造力，工具帮不上什么忙。」

正解计算器处理的是数字，证明器处理的是逻辑。证明器内部维护着一整套推理规则库和类型系统，每一条证明步骤都必须机械地映射到规则上才能通过。它不是替你「想」，但能替你「把关」——这在数学上同样宝贵，因为它从根本上杜绝了「这里显然成立」式的漏洞。工具负责的是保证每一步都脚踏实地，而不是给出灵感。

为何常见：大多数人对计算机工具的印象停留在「算得快」，而证明器的核心能力不是算得快，而是「验得严」，这种差异初接触时很难体会到。

误区「既然证明器能验证每一步，那就把所有可能的步骤都列出来，让计算机穷举到天荒地老，总能把定理证出来吧？」

正解每一步可用的 tactic 有成百上千种，搜索空间随步数呈指数爆炸——哪怕只有 20 步的证明，穷举量也远超可观测宇宙的原子数。LLM 与启发式搜索的意义恰恰在于剪枝：用直觉评估函数给路线排序，把计算资源集中在最有希望的分支上，让「碰运气」变成「有策略地排查」。盲目穷举就像侦探逐户敲完整座城市的大门，而不是先看监控锁定街区。

为何常见：人类直觉里「计算机=枚举能力强」，但枚举能力再强也追不上数学证明里组合空间膨胀的速度，这是反直觉的指数增长。

误区「这个模型的 pass@100 到了 90%，已经是顶尖数学家的水平了，以后证明定理就靠它了。」

正解pass@k 只衡量「在 k 次尝试内至少成功一次」的概率，它不衡量证明质量、简洁度、稳定性和可读性。给一个模型 1000 次机会，靠蒙也能蒙对更多题，但真正的数学研究需要的是稳定高效的推理，而不是「最终有一次撞对了」。研究者应当同时关注证明长度、单次成功率以及在陌生领域的泛化表现，而不是唯 pass@k 论英雄。

为何常见：单一指标容易给人「可排序、可比较」的错觉，人们下意识地把一个数字当成了能力的完整画像，忽略了指标背后的统计口径和任务难度差异。

面试题

Q1. 形式化证明器（如 Lean）的核心作用是什么？

单选题 · easy

  • A.自动生成数学定理，省去人工推理
  • B.严格验证证明步骤是否符合推理规则← 正确答案
  • C.把数学定理翻译成自然语言段落
  • D.替代数学家完成全部创造性的思考

答案：B。证明器是「铁面法官」，它不负责产生灵感，而是逐条检查证据链是否合法。A 和 D 把生成职责错安在证明器头上，C 则混淆了形式化表达与自然语言翻译。它真正做的是 B：对每一步推理依据规则机械校验，只有通过类型检查才算数。

Q2. LLM 在定理证明中输出的「候选证明步骤」通常以什么形式呈递？

单选题 · mid

  • A.一段情节完整的小说叙述
  • B.一条被验证过的数学定理
  • C.一条 tactic 策略指令卡← 正确答案
  • D.一个可立即运行的软件程序

答案：C。LLM 生成的是供证明器尝试的 tactic（如 intro、apply），本质上是「下一步行动指令卡」，尚未经过验证。A 是自然语言幻觉，B 混淆了输出与最终结果，D 错把 tactic 当成了可运行的独立软件。只有 C 准确描述了 LLM 与证明器交互的接口形式。

Q3. 「证明即程序」的观点出自哪个理论？

单选题 · easy

  • A.哥德尔不完备定理
  • B.贝叶斯推断理论
  • C.香农信息论
  • D.库里-霍华德对应← 正确答案

答案：D。库里-霍华德对应建立了证明与程序之间的同构关系：命题对应类型，证明对应程序，类型检查对应逻辑验证。哥德尔不完备定理讲的是公理系统的局限，贝叶斯推断处理的是概率更新，香农信息论关心的是信息度量，三者都与「证明即程序」无关，选 D。

Q4. 下面哪些属于 LLM 在定理证明中的辅助作用？

多选题 · mid

  • A.推荐优先展开哪些子目标分支← 正确答案
  • B.提出候选 tactic 供验证器检查← 正确答案
  • C.直接给出完整且必然正确的证明
  • D.根据反例反馈迭代生成新策略← 正确答案

答案：ABD。LLM 在证明闭环中扮演「出主意」的角色：推荐搜索方向（A）、生成候选 tactic（B）、根据验证器返回的反例调整后续策略（D）都是它的分内事。C 错在「必然正确」——LLM 的生成只有概率性，没有保证性，正确与否必须由验证器盖章。

Q5. pass@k 指标衡量的是什么？

单选题 · hard

  • A.证明器在一秒内执行的规则数量
  • B.k 次尝试内至少成功证明一次的概率← 正确答案
  • C.某条证明路径的完整度百分比
  • D.LLM 参数量与推理速度的比值

答案：B。pass@k 回答的是「给你 k 次机会，能不能至少一次走通真相」，它把多次尝试合并成一个概率值。A 描述的是性能吞吐量，C 描述的是单条路径的完成比例，D 更是把模型架构指标与任务评估混为一谈。只有 B 踩中了组合概率的口径。

Q6. 为什么 LLM 在长链证明中容易失败？

多选题 · mid

  • A.每一步的微小误差会随步数累积放大← 正确答案
  • B.候选证明路径的数量随步长指数增长← 正确答案
  • C.形式化证明器不支持超过十步的证明
  • D.每一环节都必须结合上下文做精确决策← 正确答案

答案：ABD。长链证明的两大敌人是误差累积（A）和搜索空间爆炸（B），而每一步决策都依赖上下文也增加了出错风险（D）。C 是事实错误——Lean 等证明器完全支持长证明，只是 LLM 撑不住长链的精度要求。整体成功率随步数连乘衰减，正是第 8 节公式揭示的道理。

Q7. 蒙特卡洛树搜索（MCTS）在证明搜索中的核心作用是？

单选题 · mid

  • A.对候选分支做模拟推演，优先展开胜算高的路线← 正确答案
  • B.把证明文本压缩成更短的数学记号
  • C.直接判定定理在直觉上是否成立
  • D.替代 LLM 生成全部候选 tactic

答案：A。MCTS 是侦探的「沙盘推演」：先随机模拟几条路线的成败，再用统计结果指导真实搜索优先走哪条，做到失败可回溯。B 是格式转换，C 是直觉判断而非搜索策略，D 把生成职能错派给了搜索算法。搜索策略负责规划，LLM 才负责提建议。

Q8. 目前 LLM 辅助定理证明相对最成熟的应用领域是？

单选题 · easy

  • A.代数与数论的形式化数学库补全← 正确答案
  • B.黎曼猜想的独立自动证明
  • C.高中平面几何的图形绘制
  • D.泛函分析的任意定理证明

答案：A。代数与数论分支拥有大量结构规整的证明和充足的形式化语料，Mathlib 等库的补全任务中 LLM 已能稳定发挥作用。黎曼猜想仍是数学界未解难题，C 只是辅助画图而非证明，泛函分析的证明形式化难度极高。选择目前工程上真正落地的领域，只能选 A。

Q9. 为什么 LLM 的建议需要配合形式化证明器使用才可靠？

多选题 · hard

  • A.LLM 可能在一本正经地产生逻辑幻觉← 正确答案
  • B.证明器能逐条校验每个步骤的合法性← 正确答案
  • C.证明器会返回反例帮助模型调整路线← 正确答案
  • D.证明器能凭空生成模型缺少的训练数据

答案：ABC。LLM 生成的证明文本没有内在的逻辑保证，随时可能幻觉（A）；证明器的逐条类型检查让错误无处遁形（B）；验证失败时给出的反例又能反馈给模型迭代修正（C）。D 夸大了证明器的能力——它不会无中生有造训练数据，只会忠实反馈校验结果。三者缺一不可，正是「侦探+法官」搭档的意义。

Q10. 要全面评估一个 LLM 证明助手的真实水平，最合理的做法是？

单选题 · mid

  • A.让几位数学教授凭感观给证明文本打分
  • B.在验证器闭环中统计最终成功率← 正确答案
  • C.对比模型生成证明的文本长度
  • D.统计模型回答问题的响应速度

答案：B。真正的能力必须放到「生成—验证」闭环里测：模型产出的候选证明是否被证明器接受，才反映它是否真的会证明。主观打分可能被流畅的叙述误导，文本长度和响应速度更是与推理能力无关。pass@k 与成功率结合，才是衡量 LLM 证明助手的科学标尺。