编辑“︁Lean简介与历史”︁（章节）

== 实际应用场景 ==
Lean 的主要应用包括：
1. '''形式化数学'''：用于构建和验证数学定理，如数学库 Mathlib 包含了数千个形式化定义和证明。
2. '''程序验证'''：确保软件的正确性，例如验证算法或协议的安全性。
3. '''教育与研究'''：用于教学编程语言理论和形式化方法。

=== 案例：验证加法交换律 ===
以下是一个在 Lean 中验证加法交换律的示例：

<syntaxhighlight lang="lean">
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a
  case zero => simp
  case succ a ih => simp [Nat.add_succ, ih]
</syntaxhighlight>

'''输出：'''
<pre>
a + b = b + a
</pre>

解释：
* <code>induction a</code> 对 <code>a</code> 进行归纳。
* <code>simp</code> 使用简化策略自动完成证明。