Lean 编程语言：用代码形式化数学

Lean 是一种编程语言，主要用于数学家将数学公式化。它允许数学家将数学视为代码，分解成结构、定理和证明，并将其放在 GitHub 上。文章通过一个简单的例子 2=2 的证明，介绍了 Lean 的语法和一些基本概念，例如 tactic（策略），并解释了如何使用这些 tactic 来证明或证伪数学命题。文章还以一个虚构的公理“2=3”为例，说明了在公理系统中，错误的公理可能导致任何结论都能被证明，突出了形式化证明的重要性。最后，文章提到了费马大定理的 Lean 形式化证明项目，作为 Lean 语言强大能力的体现。