数学能力：定理证明——AI 的奥数裁判团如何打分

可视化演示

展示从公理前提出发通过推理规则逐步构建证明链的过程、四种证明方法对比及形式化验证流程，交互调节参数观察推理深度变化。

任务定义：给 AI 出一道“可判卷”的证明题

奥数比赛的第一件事，是把题目写清楚。定理证明评测里的“题目”，不是一段模棱两可的自然语言，而是用形式化语言写成的定理陈述。比如“任意两个偶数之和仍是偶数”，必须被翻译成证明助手能识别的公式。之所以要这么严格，是因为机器裁判没有人类那种“我大概看懂了”的宽容，它只认精确符号。

模型的“答题卡”也不是一张作文纸，而是一个形式化证明脚本。这个脚本里包含每一步推理、引用的定义、使用的规则。评测系统拿到题目 \(T\) 和证明 \(p\) 后，会用验证器判断 \(p\) 是不是一个关于 \(T\) 的合法证明。这就是定理证明评测最核心的任务定义：让模型输出可以被机器验证的证明，而不是只给一个答案。

把一张模糊的“数学证明题”变成形式化定理和证明脚本，就像把一场口头争执变成有明确规则的法庭辩论。没有了“感觉上对”的灰色地带，机器才敢坐进裁判席。

证明助手：让机器当铁面裁判

小证要在奥数赛场上证明“任意两个偶数之和仍是偶数”，它不能只写一句“这是显然的”。它必须借助证明助手，比如 Lean、Coq 或 Isabelle，把证明写成一段机器能理解的交互式脚本。这里的证明助手，就是我们的“裁判长”。

为什么裁判长能保证公正？因为证明助手内部有一个很小的逻辑内核，只负责按固定的推理规则做类型检查。它不理解“巧妙”“显然”这些词，也不被步骤多少打动。内核背后是类型论：在类型论中，命题被看成类型，证明被看成该类型的项。于是，“证明一个命题”就变成了“构造一个类型正确的程序”。

裁判长不会疲劳，也不会被选手的花言巧语打动。类型论给了它一套极其简单、极其严苛的判罚手册，而小证要做的，就是在这套手册规定下，把证明一步一步搭出来。

自动验证：一条铁面无私的核查流水线

小证写完证明脚本后，比赛并没有结束，裁判长还要启动一条自动验证流水线。现实中的 Lean 等证明助手，并不是直接阅读人类友好的证明文字，而是先把证明脚本展开成更底层的证明项，这个过程叫 elaboration。展开后的证明项，再由逻辑内核做最严格的类型检查。

如果把证明脚本比作选手写的“草稿”，那 elaboration 就是把草稿誊写成标准卷面，逻辑内核则逐字检查这份卷面上的每一个推理。这一步对评测至关重要，因为验证过程必须是机械的、可复现的。只要内核给出“通过”，结果就相当于板上钉钉；一旦任何一个步骤不合规，整个证明就会被判无效。

这条流水线在真实评测里还会承载“策略生成”的玩法：模型不是一次给出完整证明，而是像下棋一样逐步生成 tactic 策略，验证器每一步都检查当前目标是否被解决。最终，所有策略合并成一个证明项导出，成为可复现的评测证据。

评分设计：不只看对错，还要看怎么证明

裁判长确认证明有效之后，主办方还要决定怎么计分。最朴素的评分方式当然是“有效得 1 分，无效得 0 分”。但真实评测往往还需要考虑：这个证明消耗了多少时间和内存？它是不是用了一个非常长的暴力搜索才碰巧过关？不同难度定理是否应该分开统计？

因此，定理证明评测的评分公式通常以正确性为第一道门槛，然后再叠加资源限制。比如设置最大运行时间 \(\tau\) 和最大步骤数，如果证明有效但超时，依然不得分。对于不同难度的定理，主办方还可以分层统计，避免“只做简单题”的模型拿到虚高分数。

这种评分设计让“走捷径”变得很难。模型不能靠死记硬背一个证明来应付所有题目，也不能靠无限暴力搜索硬磨出结果。每一项分数背后的资源约束，都在逼着模型学会更接近人类数学家的证明方式。

数据质量：别让 AI 靠背题拿高分

比赛题目册如果出了问题，那裁判再公正也没用。假设小证在训练阶段已经见过完全相同的形式化定理和对应的证明，那它上了考场只是默写答案，而不是真的会证明。因此，定理证明评测的数据质量控制，首先要做“来源筛选”：只保留有明确出处的数学竞赛题、教材定理和经典结论，并记录每道题的人工审核状态。

但仅有来源还不够，还要做“去重防泄漏”。现代大模型的训练语料非常庞大，一段数学证明可能以不同形式出现在多个网页里。评测团队需要用相似度匹配、语义去重等手段，把与训练集高度重合的题目剔除或隔离。最后，人工复核一道题的形式化翻译是否正确、证明是否真的能被证明助手接受，才能让题目正式进入评测集。

如果把定理证明大赛看成一场考试，那数据质量控制就是考前出题组的最后一道保密流程。题目质量不过关，后面所有精妙的评分规则都会变成空中楼阁。

可信保障：让不同裁判的评分对得上

一次公平的奥赛，不能只靠一位裁判拍板。定理证明评测的可信度保障，同样需要“多位裁判对得上账”。这里的“多位裁判”体现为多次运行、不同配置的复测，以及评分一致性校验。

由于证明助手内核是确定性的，理论上同一个提交会得到稳定结果。但真实系统还涉及随机搜索、设备资源波动、超时边界等问题，所以评测平台会要求模型在固定随机种子下多次运行，观察结果是否一致。如果同一个证明有时通过、有时超时，说明结果不够可信。此外，在人工参与环节里，两位专家对一道非标准题的评价也可能存在分歧，这时可以用一致性指标来衡量评分者之间的稳定程度。

为了保证可信度，赛事主办方还会给评测结果加“防作弊”机制：提交必须能被验证器重新复现，不能指向未公开的自定义公理，也不能隐藏外部记忆痕迹。当评分一致性、多次运行、防作弊三条防线同时拉满，小证的奖牌才真正经得起反复检验。

AI 应用场景

Python 演示

# 一个微型形式化证明检查器# 为方便演示，命题用字符串表示，例如 "A" 和 "A -> C" FORMAL_AXIOMS = {"A", "A -> C"} def derive_by_mp(steps, deps):    if len(deps) != 2:        return None    if deps[0] < 0 or deps[1] < 0:        return None    if deps[0] >= len(steps) or deps[1] >= len(steps):        return None    impl = steps[deps[0]]["formula"]    ante = steps[deps[1]]["formula"]    if " -> " in impl:        left, right = impl.split(" -> ", 1)        if left == ante:            return right    return None def verify_proof(theorem, proof):    for idx, step in enumerate(proof):        formula = step["formula"]        deps = step.get("deps", [])        if step["rule"] == "axiom":            if formula not in FORMAL_AXIOMS:                return False        elif step["rule"] == "mp":            if any(d < 0 or d >= idx for d in deps):                return False            got = derive_by_mp(proof, deps)            if got is None or got != formula:                return False        else:            return False    return proof and proof[-1]["formula"] == theorem def main():    proof = [        {"rule": "axiom", "deps": [], "formula": "A"},        {"rule": "axiom", "deps": [], "formula": "A -> C"},        {"rule": "mp", "deps": [1, 0], "formula": "C"},    ]    print("theorem C:", verify_proof("C", proof))    bad = proof[:-1] + [{"rule": "mp", "deps": [1, 0], "formula": "D"}]    print("theorem D:", verify_proof("D", bad)) if __name__ == "__main__":    main()

1. FORMAL_AXIOMS = {"A", "A -> C"}固定合法公理集合，相当于证明开始前裁判认可的前提条件。
2. left, right = impl.split(" -> ", 1)把蕴含式拆成前件和后件，完成一次 MP 规则里的“对号入座”。
3. if any(d < 0 or d >= idx for d in deps):确保每个步骤只能引用前面已经产生的结论，杜绝循环论证。
4. if got is None or got != formula:如果推导结果和声明不一致，证明立刻被判错。
5. return proof and proof[-1]["formula"] == theorem证明的最后一行必须与题目中的定理完全一致，一个字符都不能少。

常见误区

面试题