数学能力：定理证明Lean

可视化演示

三步展示Lean定理证明器：小可信基内核+策略架构、Prop/Type/Π类型依赖类型宇宙、以及目标→策略→校验的证明交互评测流程。

Lean定理证明器：工地上的铁面监理

假设你家的装修工程请了一位铁面监理——他不听你解释，不看你的施工许可证，只认手里的检测仪器。你说“线管已经埋好了”，他就拿摇表测绝缘；你说“水管不漏”，他就上压力泵打压测试。一切以仪器读数说话。Lean 定理证明器就是数学世界的这种铁面监理：它不关心你说得多么振振有词，只关心你给出的证明步骤能否符合逻辑规则。

Lean 是一个交互式定理证明器，它建立在一种叫作“依赖类型论”的数学基础之上。通俗地讲，Lean 把每一个数学命题都编码成一种“类型”，而证明这个命题就等价于构造出一个该类型的“实例”——就像监理把“电路绝缘合格”定义为一套测试标准，你要做的就是让实测结果落入标准允许的区间。这就是“证明即程序”的直观含义：一个证明在 Lean 中就是一个可以被核验的数据对象。

在 Lean 的世界里，有一个巨大的数学知识库叫 Mathlib，它收集了从基础算术到现代代数几何的大量已证明定理。当 AI 模型试图证明一个新定理时，它可以像装修师傅调用标准件一样，调用 Mathlib 里已有的结论作为跳板，而 Lean 则确保每一块跳板都安装牢固。

就像监理不会替工人搬砖，Lean 也不会替模型想证明思路——它只负责严格检查。但正因为有了这道铁面无私的关卡，AI 的数学能力才第一次有了“无法注水”的考核方式。

证明任务构造：把毛坯房画出施工图

要让监理开工，首先得有图纸。在 Lean 评测中，“图纸”就是证明任务——把一个自然语言描述的数学命题翻译成 Lean 能理解的形式化语言。这就像把“我要在客厅装三个插座”翻译成带坐标、带管线走向的施工图。

构造证明任务的第一步是“命题形式化”。以“所有偶数都能被 2 整除”为例，自然语言里有歧义，但 Lean 要求写成精确的逻辑表达式。第二步是明确“目标与前件”——目标的结论是什么、前件有哪些已知条件。第三步是将数学对象（比如“偶数”“整除”）翻译成 Lean 内核中的定义。最后，根据难度给任务分层：有的只是单步推理，有的需要复杂的归纳构造。

施工图画得好不好，直接决定了后面施工顺不顺。同样地，证明任务的形式化质量直接决定评测的公平性——任务若含糊其辞，模型就无法稳定发挥；任务若严谨清晰，模型的每一步都能被精确打分。

证明状态表示：工地进度板的精确刻度

走进任何一家规范的施工工地，你都会看到一块进度板，上面写着每个工序的状态：管道铺设中、防水测试待检、瓷砖铺贴完成。在 Lean 中，这块进度板就是“证明状态”。模型在证明的每一步都会看到当前的状态，然后据此决定下一步动作。

一个典型的证明状态长这样：上方是一个待证目标的列表，下面是一些局部上下文变量。比如在证明“若 a 是偶数则 a^2 也是偶数”时，上下文里会列出已知条件“a 是偶数”，而目标则是“a^2 是偶数”。模型每执行一个策略，Lean 就更新一次状态——就像工人每完成一个工序，监理就在进度板上打一个勾。

进度板让工人和监理共享同一份事实，而证明状态则让模型和 Lean 对齐“当前进展”。这种透明的状态表示是“AI 与证明助手协作”的基础——没有它，模型就只能摸黑猜，根本谈不上系统化的推理能力。

模型交互流程：AI模型与监理的回合制博弈

现在，装修队正式进场了。我们把 AI 模型想象成施工队长，Lean 是监理。两者的互动是一个清晰的循环：施工队长提出一个施工方案（生成策略），监理检查方案是否合规（Lean 执行校验），如果合规就更新工程进度（状态回传），如果不合规就打回重来。如此反复，直到整个工程完成。

每一步交互在技术上是这样发生的：模型输入当前的证明状态和可选的历史信息，输出一个策略（比如“induction n“或”apply h“）。然后 Lean 执行这个策略，产生新的证明状态或报错信息。这条反馈回路让模型得以”试错—学习—逼近”—就像一个施工队长通过不断微调方案来满足监理的要求。

这个回合制交互流程设计的关键在于：模型的每次尝试都被 Lean 即时验证，让它无法蒙混过关。这就像施工队和监理之间的每一次对话都以实测数据为准，磨洋工、耍嘴皮在工地上没有生存空间。

评测效果评估：拿什么给 AI 的数学能力打分

工地竣工了，如何评估装修队的水平？显然不是听队长吹嘘自己“手艺精湛”，而是看几个硬指标：工程是否按时交付、验收一次通过率多高、返工次数多少。评估 AI 在 Lean 上的表现，同样需要多维度的硬指标。

首要指标是“证明成功率”：在给定的测试题目中，模型能在有限步数内完成证明的比例。其次是“平均策略步数”：模型平均用多少步完成一条证明——步数越少通常意味着效率越高。此外，评测还要与人类基线对比：同样一批题目，AI 的表现与专业数学家相比如何？最后，不同难度等级的题目要分类报告，以免模型只会做简单题却标注为“全能型选手”。

多维度的评估让我们既看到 AI 能做什么，也看到它做到什么水平。就像装修队的口碑不只看完工照，还要看在隐蔽工程中的实际做工——成功率、步数、难度分层共同绘制了一幅更真实的 AI 数学能力画像。

可信度保障机制：如何让“AI 数学成绩单”可信

一张满分的成绩单如果由考生自己批改，任何人都不会相信。同样的道理，“AI 在 Lean 上取得了 X% 成功率”这个结论要可信，必须在数据、评分、防作弊三个层面都设好关卡。

第一道关卡是“数据质量控制”。用于评测的题目必须经过人工审核，确保形式化正确、难度标注合理、没有语法垃圾。第二道关卡是“评分一致性校验”：不同的评分方式（如 LLM 评分与规则评分）之间要交叉验证，确保结论不因评分机制的偏差而失真。第三道关卡是“训练集防泄露”：确保测试题目没有出现在模型的训练语料中，否则就是“考生提前拿到考卷”。最后还有“双重验证机制”：关键的评测结论至少经过两种独立方法的确认，才能发布。

这些机制相当于给 AI 评测系统装上了多重保险：数据干净、评分公正、考卷不外泄。每一条都在回答同一个问题——我们凭什么相信这份成绩单？监理当然要讲人情，但工程验收只相信数据和规范。同样，AI 能力的评测也必须用这种工程化的严谨态度来守护可信度。

AI 应用场景

Python 演示

import re class SimulatedLean:    """模拟 Lean 的验证器角色"""    def __init__(self):        self.context = ["n : Nat", "h : n > 0"]  # 已知前件     def check_tactic(self, tactic, state):        """验证策略是否合法"""        if tactic == "apply h":            new_goal = "n > 0"            return True, new_goal, "目标已满足"        if tactic == "exact h":            return state == "n > 0", None, "利用前提直接证明"        if tactic.startswith("rewrite"):            q = tactic.split("rewrite ")[-1]            if q in self.context:                return True, None, "重写成功，目标已消除"            return False, state, "重写失败：未知引理"        return False, state, "策略格式错误" class TacticModel:    """模拟一个简单的策略生成模型"""    def __init__(self, candidates):        self.candidates = candidates     def predict(self, goal):        # 按候选顺序尝试策略        for c in self.candidates:            yield c def main():    lean = SimulatedLean()    model = TacticModel(["apply h", "exact h", "rewrite h"])    goal = "n > 0"    max_steps = 5    print("=== 模拟 Lean 证明交互 ===")    for step in range(max_steps):        print(f"目标: {goal}")        tactic = next(model.predict(goal), None)        if tactic is None:            print("无可用策略，证明失败")            return False        print(f"模型提出策略: {tactic}")        ok, new_goal, msg = lean.check_tactic(tactic, goal)        if not ok:            print(f"Lean 拒绝: {msg}")            continue        print(f"Lean 反馈: {msg}")        if new_goal is None:            print("=== 证明完成 ===")            return True        goal = new_goal    print("步数超限，证明失败")    return False if __name__ == "__main__":    success = main()    print("最终结果:", "通过" if success else "未通过")

1. class SimulatedLean:用 Python 类模拟 Lean 的角色，每个 check_tactic 方法就是一条验证规则。
2. def check_tactic(self, tactic, state):这是整个模拟的核心：模型提出的策略必须过这一关，非法策略会被拒绝。
3. model = TacticModel(["apply h", "exact h", "rewrite h"])模拟模型根据概率排序的策略候选集。
4. tactic = next(model.predict(goal), None)模型从候选中选出当前最佳策略。
5. ok, new_goal, msg = lean.check_tactic(tactic, goal)执行校验并获取反馈。

常见误区

面试题