几年前，数学家 Kevin Buzzard 有了一个令人不安的认识：数学依赖于信任——信任证明是正确的，信任审查员会发现错误，信任错误不会被忽视。
但是如果这种信任失效了呢？
在他的职业生涯中，Buzzard 不得不与许多研究人员争论，尽管存在明显的缺陷，但他们拒绝承认他们的证明是错误的！ 最终，这让他失去了对“人工检查”数学的信任。
对于像 Buzzard 这样的数学家来说幸运的是，交互式定理证明器——也称为 证明助手——正在兴起。 这些工具能够创建严格的、机器可检查的数学定理和计算的证明。
相信人类？ 不再需要了！
除了在纯数学中的应用，证明助手在应用密码学中也变得越来越重要。 例如，在 zkSecurity，我们利用它们来开发用于 zkVM 的形式验证工具。
在这篇文章中，我们将为你提供一个对初学者友好的证明助手介绍，并向你展示如何开始使用它们来构建坚如磐石、机器验证的论证。
为什么选择证明助手？
证明助手可以帮助你验证数学证明是否“可以编译”。 事实上，证明助手中的证明检查与传统编程语言中的类型检查完全相同。
换句话说，一位提出定理新颖而复杂证明的数学家可以（而且可能应该）使用证明助手来确保证明中的每一步逻辑都是有效的。 如果证明通过了助手的检查（假设信任该工具本身），那么数学家就可以确信他们的推理是正确的，并且没有逻辑错误。
以 Peter Scholze 为例。 在 2020 年 12 月的一篇博客文章 中，这位菲尔兹奖获得者数学家承认，他不确定他对以下消失定理的证明的有效性：
定理 设 0<p′<p≤1 为实数，设 S 为一个 profinite 集合，设 V 为一个 p-Banach 空间。设 Mp′(S) 为 S 上的 p′-测度的空间。那么
$ExtCond(Ab)^i(M_{p'}(S),V)=0$
对于 i≥1。
引用 Scholze 的话：
我花了 2019 年的大部分时间沉迷于这个定理的证明，几乎为此发疯。 最后，我们能够在纸上确定一个论证，但我认为没有人敢去看其中的细节，所以我仍然有一些小的挥之不去的疑虑。 […] 我认为这可能是我迄今为止最重要的定理。 […] 最好确定它是正确的……
一年半后，Scholze 的证明通过证明助手进行了形式化，消除了他对证明正确性的剩余疑虑。
证明助手 vs. 传统方法
交互式定理证明器提供的能力是传统测试或手动编写证明难以或不可能实现的：
- 严谨性： 它们确保每一步逻辑都有效，并与形式规则一致。
- 穷尽性： 与检查特定情况的测试不同，证明助手确认所有输入和条件下的正确性。
- 错误预防： 通过在开发/证明构造阶段发现错误，证明助手可以防止错误传播到现实世界的应用中。
Lean：现代证明助手
虽然有许多不同的证明助手可用，但 Lean 近年来获得了显著的关注。 其丰富的 mathlib 库和活跃的社区使其成为任何希望深入研究交互式定理证明的人的绝佳起点。 因此，本文的剩余部分将侧重于 Lean。
一个简单的例子
让我们用一个简单的例子来说明 Lean 的功能：
theorem binomial_theorem (a b : ℝ) : (a + b)^2 = a^2 + 2 * a * b + b^2 :=
calc
(a + b)^2 = (a + b) * (a + b) := by
rw [pow_two]
_ = a * a + b * a + (a * b + b * b) := by
rw [mul_add, add_mul, add_mul]
_ = a * a + (b * a + a * b) + b * b := by
rw [← add_assoc, add_assoc (a * a)]
_ = a * a + 2 * a * b + b * b := by
rw [mul_comm b a, ← two_mul, ← mul_assoc]
_ = a^2 + 2 * a * b + b^2 := by
repeat rw [← pow_two]
第一行定义了我们旨在证明的恒等式：(a + b)^2 = a^2 + 2 * a * b + b^2。 在 calc 块中，我们将等式的左侧转换为右侧，利用 Lean 标准库中提供的中间数学定理，如 pow_two 和 mul_add。
特别是，我们不在没有理由的情况下假设 a * b = b * a 这样的属性。 相反，我们必须显式地调用 mul_comm 定理 来使用实数在乘法下形成交换 magma 这一事实。 这种形式化的方法确保了证明严格地建立了每一步骤，包括 a * b = b * a，作为实数数学结构的直接结果。
动手体验 Lean
Lean 4 拥有强大的社区，并提供许多不同的交互式定理证明的切入点。 如果你刚刚开始，我们建议你执行以下操作：
- 观看 Terence Tao 的 关于机器辅助证明的 50 分钟演讲。
- 加入 Lean Zulip 在线聊天群。
- 玩 自然数游戏，以游戏化的方式学习基础知识。
- 完成 Lean 中的数学。
所有这些资源都假定对数学有基本的熟悉，但不需要高级知识。 特别是，不需要形式化方法的先验知识。
zkVM 开发中的证明助手
像 Lean 这样的证明助手在验证零知识虚拟机 (zkVM) 的正确性方面发挥着越来越重要的作用，而仅通过传统的测试方法来验证这些虚拟机可能具有挑战性。
像 Lean 这样的工具使我们能够证明关键 zkVM 组件的正确性，例如算术电路、密码学原语和状态转换。 这种形式化的方法确保了这些组件在所有条件下都按预期运行，为 zkVM 的可靠性提供了更强大的基础。
因此，我们计划发布更多文章，探讨证明助手如何应对 zkVM 开发中的特定挑战。 敬请关注！
