企业官网建设流程全解析

Superhuman的LeanProofBench教程：Lean 4数学形式化入门实战

【免费下载链接】superhuman项目地址: https://gitcode.com/GitHub_Trending/sup/superhuman

想用Lean 4学习数学形式化证明，却不知道从哪里下手？本文以 Google DeepMind 开源项目Superhuman中的IMO-LeanProofBench为蓝本，带你完成一场 Lean 4 数学形式化入门实战：读懂一道被 Lean 4 精确刻画的数学题，拆解它的完整机器可验证证明，并建立自己的练习路线 📚

什么是 LeanProofBench？

LeanProofBench是 Superhuman 项目中 IMO Bench 基准套件的数据集之一，由 Google DeepMind 的 Superhuman Reasoning 团队发布。它收录了60 道国际数学奥林匹克（IMO）风格的证明题，并且每道题的题干都被数学专家翻译成了 Lean 4 的形式化语句。

它的核心数据文件是 lean_proof_bench.csv，包含题目、标准解答、评分标准、难度等级和Lean Statement（Lean 4 形式化题干）等字段。难度分布为：

对新手来说，这是少有的"从入门到竞赛级"难度平滑的 Lean 4 证明题库。

第一步：看懂一道 Lean 4 数学题

传统数学题用自然语言描述，而 Lean 4 要求把每一个数学对象、每一个条件都写成精确的类型和命题。以题库中的第一道题 PB-Basic-001 为例，原题是：

求所有函数 $f:\mathbb{Z}\to\mathbb{Z}$，使得对一切 $x,y$，有 $f(2x)+2f(y)=f(f(x+y))$。

它的 Lean 4 形式化题干（节选自数据文件的 Lean Statement 列）长这样：

theorem PBBasic001 : {f : ℤ → ℤ | ∀ x y, f (2 * x) + 2 * f y = f (f (x + y))} = {0} ∪ {(fun x ↦ 2 * x + c) | (c : ℤ)} := by ...

对照原题目，你会发现 Lean 4 的写法非常直白：

• f : ℤ → ℤ—— 定义域和值域都是整数
• ∀ x y, ...—— "对一切 x, y"
• 等号右边用集合等式直接写出了答案：零函数，或形如 $f(x)=2x+c$ 的函数

这正是形式化证明的魅力：把"证明这道题的答案是它"变成让编译器逐行核验的逻辑任务。

第二步：拆解一份机器验证过的完整证明

Superhuman 仓库里的 leap/solutions/ 目录提供了 Lean 4 完整解答，全部通过了编译验证。文件 PBBasic001_solution.lean 展示了经典的"引理拆解"风格——主定理不一步到位，而是被拆成一条条小引理：

theorem PBBasic001_lem3 (f : ℤ → ℤ) (h : ∀ x y, f (2 * x) + 2 * f y = f (f (x + y))) (x : ℤ) : f (2 * x) = 2 * f x - f 0 := by have h1 := h x 0 have h2 := h 0 x rw [add_zero] at h1 rw [zero_add, mul_zero] at h2 omega

几个新手高频技巧值得注意：

• have h1 := h x 0：把全称条件实例化到具体取值，是处理函数方程的第一反应
• rw [...]：重写等式，像代数消元一样一步步化简
• omega/linarith：调用自动求解器收尾整数线性推理
• 引理命名规范：PBBasic001_lem3这样的命名让长证明依然可检索、可复用

整个证明从"推出 $f(2x)=2f(x)-f(0)$"出发，经归纳法、正负整数分类讨论，最终收敛到主定理的集合等式，结构清晰，非常适合作为入门范本。

第三步：为什么形式化让评分更可靠？

自然语言证明的评分长期依赖人工阅卷，而 Lean 4 编译器给出了"对/错"的机器判据。IMO Bench 的评测图表显示，各模型在 LeanProofBench 上的自动评分与人工评分高度一致，基础题组中领先模型的准确率可超过 80%，而进阶题组普遍跌至 60% 以下——难度分级被证明力数据真实地刻画了出来。

新手上手清单：从克隆到独立解题

1. 获取仓库：执行git clone https://gitcode.com/GitHub_Trending/sup/superhuman，进入项目浏览结构
2. 打开题库：用表格工具打开 lean_proof_bench.csv，从Level为pre-IMO的 8 道题开始
3. 对照学习：每做一题，先自己写 Lean 4 证明，再对照 Basic 解答集 和 Advanced 解答集，理解引理拆分与rw、induction、omega等战术的使用
4. 进阶挑战：阅读 LEAP 框架介绍，了解"AND-OR 分解 + 编译器反馈"的自动证明思路，并可尝试 Putnam 2025 全量解答 中的 12 道正式赛题
5. 视野拓展：Aletheia 目录收录了 Gemini Deep Think 攻克研究级数学问题的 LaTeX 论文原文，是形式化之外的延伸读物

💡 小贴士：Lean 4 的import Mathlib会带来庞大的数学库，编译较慢是正常现象；初学阶段建议把注意力放在"命题如何陈述"和"引理如何递推"上，战术细节可交给自动求解器。

写在最后

LeanProofBench 用 60 道题搭起了一座桥梁：一端是 IMO 的数学语言，另一端是 Lean 4 的严谨世界。跟着本文的三步走——读题干、拆证明、跟评分——你就能在几周内建立起对数学形式化的手感。当你的第一份.lean文件打出sorry并被逐步消灭时，机器可验证的证明之路才算真正开始 🚀

【免费下载链接】superhuman项目地址: https://gitcode.com/GitHub_Trending/sup/superhuman