> ## Content Index
> Fetch the complete content index at: https://www.hubwiz.com/blog/llms.txt
> Use this file to discover other available public pages before exploring further.

# Lean 简明教程
- URL: https://www.hubwiz.com/blog/a-concise-tutorial-on-lean/
- Published: 2026-09-30T17:19:09.000Z
- Updated: 2026-09-30T17:19:09.000Z
- Description: 一门能证明数学的语言
- Author: admin
- Tags: INDUSTRY, LEAN, #Import 2026-10-14 14:41

不久之前的 2026 年 9 月，OpenAI [宣称](https://openai.com/index/navier-stokes-solution/?ref=hubwiz.com)他们解决了千禧年大奖难题之一——描述粘性流体运动的 Navier–Stokes 方程。对我们来说更有趣的是：这份证明是用编程语言 **Lean** 写的，并且 [已在 GitHub 上公开](https://github.com/openai/NavierStokesAndEuler?ref=hubwiz.com)。

作为一名软件开发者，我此前从未用过 Lean，但读到这条新闻后，我很好奇它是如何工作的。于是决定在 Lean 里写一个简单的 "Hello World"，顺便证明两个中学水平的小定理。

开始吧！如果你对"实战"编程过程感兴趣，文章末尾也附上了 [视频](https://youtu.be/nK-DbfTmYtw?ref=hubwiz.com)。

## 1\. 勾股定理

我们从简单的内容开始——勾股定理。它很简单，希望大家都认识。假设我们有一个直角三角形：

![直角三角形](https://www.hubwiz.com/blog/content/images/2026/09/1-Kh_Eq3bXrKJq1FIC28r5Ig-1.png)

勾股定理指出：

> C² = A² + B²

如果你做过哪怕一个电脑游戏，大概率已经频繁用这个公式计算两点之间的距离了。

那我们该如何在 Lean 中证明它呢？

首先，Lean 并不会替我们证明定理，但它可以 *验证* 证明。所以，我们需要先自己构造一个证明。对勾股定理来说这很容易：画四个三角形，再加一个边长为 C 的正方形：

![勾股定理证明图](https://www.hubwiz.com/blog/content/images/2026/09/1-jTstzJMp2P6CUuOxRxrqxQ-1.png)

于是大正方形的面积是 (A + B)²。它同时也等于内部正方形 C² 加上四个面积各为 1⁄2AB 的三角形。把这些写在一起：

> S = (A + B)² = (A + B)(A + B) = A² + 2AB + B² S = C² + 4\*1⁄2AB = C² + 2AB C² + 2AB = A² + 2AB + B² => C² = A² + B²

希望这看起来足够简单。但想象一个有 5 页证明的大型定理——我们能否用编程语言把证明形式化地写出来，让计算机验证它是否正确？答案是可以的，而这正是 Lean 被设计出来的目的！

从外观上看，它有点像 Python。首先我需要导入库：

```
import Mathlib.Basic.Real.Basic
import Mathlib.Tactic.Ring

```

这里，[Ring](https://leanprover-community.github.io/mathlib4%5Fdocs/Mathlib/Tactic/Ring/Basic.html?ref=hubwiz.com) 是一个数学求解器，可以化简公式、展开括号，并完成其他常规代数运算。而 *Real* 是实数的基本数据类型。现在，我们可以声明一个 *定理*（theorem）：

```
theorem pythagoras_algebra (
  a b c : Real
) (h : c^2 = (a + b)^2 - 4 * (a * b / 2)) : c^2 = a^2 + b^2 := by

```

其中，*a*、*b*、*c* 是数据输入；`c² = (a + b)² — 4 * (a * b / 2)` 是我已有的假设，而 `c² = a² + b²` 是我希望由该假设推出的结论。

接下来，我来写实际的证明主体：

```
  calc
    c^2 = (a + b)^2 - 4 * (a * b / 2) := h
    _   = a^2 + 2 * a * b + b^2 - 2 * a * b := by ring
    _   = a^2 + b^2 := by ring

```

这里我逐行写出等式，关键字 `by` 让 Lean 知道 Ring 求解器可以检查这一步。例如，它能验证 *(a + b)² — 4 \* (a \* b / 2)* 确实等于 *a² + 2 \* a \* b + b² — 2 \* a \* b*。

每个人都可以在 [https://live.lean-lang.org](https://live.lean-lang.org/?ref=hubwiz.com) 上花 5 分钟在线体验 Lean，把完整代码粘贴进去即可：

![Lean 在线编辑器](https://www.hubwiz.com/blog/content/images/2026/09/1-jVIRLyF1gWDQwjsSii3hvw-1.png)

右侧的 Lean 输出显示 "No goals"，意味着定理的各部分都已证明完毕。如果出现任何数学错误，Lean 会停下来并给出提示信息。

到这里就能看到最终结论了：只要我们能用 Lean 写出定理，证明的验证就可以自动完成。证明代码也可以发布、放进代码库、用于证明其他定理，等等。

## 2\. 半圆的长度

接下来，我们试一点不同但同样有趣的内容。你觉得哪条曲线更长——黑色还是蓝色的？

![半圆长度对比](https://www.hubwiz.com/blog/content/images/2026/09/1-Q96AWiQy117f0bjlm_TNTQ.png)

我们用 Lean 来证明它们相等。首先，圆的周长是 2πR，所以黑色曲线的长度是 π(A + B)/2，而蓝色曲线的总长度是 πA/2 + πB/2。因此可以写成：

> L1 = π(A + B)/2 L2 = πA/2 + πB/2

希望对任何在学校上过至少一节数学课的人来说，L1 = L2 都很明显。我们用 Lean 写出来：

```
theorem circles (
    a b l1 l2: Real
) (h1 : l1 = π * (a + b) / 2) (h2 : l2 = π * a  / 2 + π * b / 2) : l1 = l2 := by
  -- Substitute l1, goal is: π * (a + b) / 2 = l2
  rw [h1]
  rw [h2]
  ring

```

这里，`rw`（rewrite，重写）关键字告诉 Lean 将 *h1* 替换为它的定义 `π * (a + b) / 2`，对 *h2* 同理。然后我们调用 Ring 求解器，验证两个等式相等。

在 Lean 中运行这段代码后，系统显示 "no goals"。证明是正确的：

![证明已验证](https://www.hubwiz.com/blog/content/images/2026/09/proof_verified.png)

## 3\. 编写 "Hello World"

可以看到，我们能在 Lean 中证明定理。那我们还能不能编写并运行"经典"应用程序呢？当然可以。首先，我创建一个名为 "triangle" 的项目：

```
lake init triangle

```

这种语法大概是受 make 的启发。举个例子，我来写一个方法，检查三角形的各边取值是否正确：

```
def test_triangle (a b c : Int) : IO Unit := do
  -- The '==' checks for boolean equality at runtime
  if a^2 + b^2 == c^2 then
    IO.println s!"Success: {a}^2 + {b}^2 = {c}^2 is TRUE"
  else
    IO.println s!"Wrong: {a}^2 + {b}^2 = {c}^2 is FALSE"

```

这门语言看起来像 Python 和 Turbo Pascal 的奇怪混合体，但又有何妨呢？ 现在，我们添加一个 "main" 函数，并测试两组三角形：

```
def main : IO Unit := do
  IO.println "Testing numbers..."

  -- This will print Success
  test_triangle 3 4 5

  -- This will print Wrong
  test_triangle 4 5 6

```

最后，我们可以运行 *lake build* 来构建项目，再用命令 *lake exe triangle* 执行它。可以看到，程序运行成功了：

![Hello World 运行结果](https://www.hubwiz.com/blog/content/images/2026/09/1-b4rCWP6dAYLH5nZPASttEw.png)

显然，Lean 也有 GUI 库，所以理论上它能运行 Doom——欢迎读者自行验证 :)

## 4\. 结束语

在本文中，我体验了编程语言 Lean。作为一名软件开发者，我大概永远不会在生产环境中使用它，大多数读者也是如此。尽管如此，测试 Lean、了解它如何工作，还是相当有趣的。

---

原文链接: [Making a "Hello World" in Lean](https://freedium-mirror.cfd/https://levelup.gitconnected.com/making-a-hello-world-in-lean-10871f2b93c3?source=home%5Ffor%5Fyou---------7-102--------------------aedc41f4%5F9c81%5F4290%5F85aa%5F557300b7e844-------15---------)

汇智网翻译整理，转载请标明出处