INDUSTRY

Lean 简明教程

一门能证明数学的语言

admin

• 6 min read
Lean 简明教程
博途PLC工程智能体 | AI智能体博途网关 | 梯形图转SCL | 自然语言生成梯形图 | 自然语言生成SCL | 逆向生成程序块文档 | 梯形图在线查看 | 博途编程文档MCP | AI模型价格对比 | AI工具导航 | ONNX模型库 | Vibe Coding教程 | PLC在线仿真器 | Tripo 3D | Meshy AI

不久之前的 2026 年 9 月，OpenAI 宣称他们解决了千禧年大奖难题之一——描述粘性流体运动的 Navier–Stokes 方程。对我们来说更有趣的是：这份证明是用编程语言 Lean 写的，并且 已在 GitHub 上公开。

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

开始吧！如果你对"实战"编程过程感兴趣，文章末尾也附上了 视频。

1. 勾股定理

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

直角三角形

勾股定理指出：

C² = A² + B²

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

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

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

勾股定理证明图

于是大正方形的面积是 (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 是一个数学求解器，可以化简公式、展开括号，并完成其他常规代数运算。而 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 上花 5 分钟在线体验 Lean，把完整代码粘贴进去即可：

Lean 在线编辑器

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

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

2. 半圆的长度

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

半圆长度对比

我们用 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"。证明是正确的：

证明已验证

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 运行结果

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

4. 结束语

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

原文链接: Making a "Hello World" in Lean

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