简谈Lean的使用

心情: 好奇

标签: Lean, 形式化, AI, 数学, 证明, 编程语言

前言

Lean是一个微软工程师拿C++写的证明器，由于其几乎所有内容专为数学证明而生，所以在数学圈非常流行。

特别是这玩意AI用起来方便，现在AI用Lean证明数学定理已经有多个成功案例。

至于原理，计算机怎么就能拿来证明抽象的数学内容了？这要追溯到上世纪图灵的老师Alonzo Church提出的Lambda Calculus，简单来说就是虽然我没懂他怎么做的反正结果上证明了只靠函数可以模拟几乎所有数学，至少古典是这样，这在后来催生出无数函数式编程语言的设计。

其中最出名的就是用一个非函数的任意符号表示0，下一个数的定义就是把这个数外再嵌套一层函数，递归的我们就完全抽象的定义了自然数。比方说我们用f表示函数，ZERO表示0，那么f(ZERO)表示1，f(f(ZERO))表示2，以此类推。也有麻烦的地方，计算机这里的函数均是接收值后返回值，单向操作，不支持逆映射，你无法简单的把数字变成上一个，只能从头开始一个个检查下一个，到下一个数与待回退数一样的时候才知道手上拿着的是上一个数字。

至于这么表示有什么好处之类的问题，这里就不作展开了，因为我也不大明白，毕竟我平时也没遇到过什么东西非要表示成计算机可验证的抽象形式。

说完大概的原理，这篇文章讲一下Lean怎么用。至于我手上又没有什么研究成果形式化了会更高大上些为啥要碰Lean，因为学校老师说想学但此前尝试没能学会，这东西也确实有意义，虽然作为编程语言是失败的，但是作为数学证明器和AI工具它非常成功。连大学教授都有没能掌握Lean的，我觉得肯定也有很多对数学感兴趣或者从事数学相关工作的人希望使用Lean但不会用，或者说没学会。

我去看了Lean的官网，教程非常多，API参考也是一套一套的，但我点进去才明白，这Lean的官方文档和Rust社区一样遵循的是全自动策略，特别是API参考，明显只是程序通过函数签名自动生成的，这也配叫文档？Rust有个非常牛逼的功能，就是它可以自动通过你的程序注释和函数签名生成文档，听起来很厉害吧，实际没人看，因为这个文档存在的唯一目的就是存在本身，根本不是为了教会人怎么用，有这功夫去翻源代码甚至发邮件问作者早解决了。

不过呢，Rust开发者特别喜欢给自己的小项目专门搭主页，生怕路过的人注意不到他那猫娘头像的推特帐号，在这些项目主页里就能看到真教程。可惜玩Lean的主要是搞AI的和搞数学的，没有专门写教程这一说。

那么，Lean为什么能得到数学界的信任呢？因为它从设计上就是跑通即正确，你用它的形式化证明工具，甭管中间走了多少条命令，改了多少东西，只要结果到了，就一定是对的。这也是为什么AI都用它玩抽象证明，反正我们只关注结果，它用一万页证明还是一百页证明没有区别，过程是有点黑盒，但我们确信是正确的。

Lean是很必要吧，我也觉得有必要作为博客教程啊，下面开始。当然了，我不会涵盖所有Lean的使用，也没那个兴趣，仅lean本体和mathlib啊，其它方面的使用不在介绍计划内。

正文

安装

建议初学阶段直接用在线版。主要是lean的实际安装也和rust一个鸟样，绑编辑器还绑下载管理器，这种远程一键安装脚本的不用理会，反正在线用也是够的，只有拿这玩意写程序才需要本地装。完全不会用还花个把小时搭环境和连AI是什么都第一次听说也要跟着装龙虾没有区别，都是差生文具多。

这里是需要开wasm权限的，浏览器没有明显报错的话不用理我这句话。

不过我接下来按本地安装讲啊。

假设你像我一样装了lean4本体，没有弄编辑器、elan、lake什么的。这当然在长期使用是不推荐的，但是就学习而言和学怎么写lean无关的内容越简单越好。

官网上没有说怎么只装lean4，不过我们去原仓库的发布部分可以下载到，写这篇文章时最新的是4.33.1版本，苹果下darwin，微软和linux自然知道，aarch64是arm架构。我这篇博客使用的是4.29.0版本，但一般来说你不必和我一致，用最新的就可以了。

是压缩包，下载下来解压，本文只使用其中的lean和lake命令。苹果和linux应该需要给可执行权限，windows的话可能是lean.exe之类的，执行的时候允许一下即可。

测试可用性

在实际开始之前让我们测试一下是否可用。

新建一个文本文件并输入如下内容

#eval 1+2

接下来，将这个文本文件的路径作为参数传递给lean命令，在windows上可能这个lean命令只是指向lean可执行文件的路径，之后我们就不作区分了。

比如，你的文本文件命名为test.lean，然后运行lean test.lean或者.\lean.exe C:\User\Document\test.lean之类的东西，应该会看到输出3。

如果没有看到，你安装有问题，看到了，那么可以直接去看下一节。

不知道有没有人不会开命令行的，在windows文件夹界面按住shift右键可以选择在Powershell内打开此文件夹，苹果和linux不会开的建议去用windows。

熟悉一下lean

在摸mathlib前，我们先做一个编程语言入门的传统艺能，说HelloWorld的可以出去了。

当然是随机一个1-100的数字，你去猜，计算机告诉你每次的大小，最后猜对时输出你猜测次数。

请把test.lean内容替换成

import Std

partial def gameLoop (stdin : IO.FS.Stream) (secret : Nat) (attempts : Nat) : IO Unit := do
  IO.println "Guess a number from 1 to 100."

  let input ← stdin.getLine
  let input : String := (String.trimAscii input).toString

  match String.toNat? input with
  | none =>
      IO.println "Please enter a whole number."
      gameLoop stdin secret attempts

  | some guess =>
      if guess < secret then
        IO.println "too small"
        gameLoop stdin secret (attempts+1)
      else if guess > secret then
        IO.println "too big"
        gameLoop stdin secret (attempts+1)
      else
        IO.println "correct!"
        IO.println s!"you guessed {attempts+1} times in total"

def main : IO Unit := do
  let stdin ← IO.getStdin
  let secret ← IO.rand 1 100
  IO.println "secret picked"
  gameLoop stdin secret 0

请注意，不能有tab占位，所有缩进用空格实现，文件用ASCII或UTF编码。

由于本文重点不是教如何用lean写一般程序，而是lean在数学方面的使用，所以我就不细说这个1-100猜数游戏怎么就这么写了。

大体上逐行意思如下：

  1. 为了使用IO模块（input/output，输入输出），引入标准模块

  2. 部分的定义函数gameLoop，接受三个输入参数，第一个是类型为IO.FS.Stream，也就是IO模块下文件系统模块的流，文件流，比方说播放音乐时电脑可能是流式的读取某个音频文件，第二三个类型均为Nat自然数，输出一个被IO类型转换的任意值（Unit在lean这里就是任意的值，跟基类差不多）

    什么是partial，属于lean特色，它默认所有函数是可以在得到参数输入时知晓能否结束的，但是我们这里函数能否结束取决于用户的命令行输入，函数被调用时永远不知道能否结束，所以需要加partial来告诉lean这个函数不是我写错了，它就是这样设计的，没法机械的判断能否终止。

  3. 打印出猜数字要求

  4. 声明一个本地变量input，进行读取一行输入的行为，并将行为结果（你在命令行输入并回车提交的字符串）赋值给input

    声明赋值的时候，后面是Action行为我们用箭头，后面是现成的值（如函数返回）的话就用赋值符号:=，你可以理解为lean不知道Action行为会多久结束，箭头可以让它等到拿到行为输出值再赋值并继续。只不过这是严格且强制的，你乱换用lean就报错了。

  5. 用String库的函数去掉换行符号并转化为字符串，函数返回值设定为新的input本地变量，且我们要求这个本地变量类型是String，不是则lean应当报错而不是沉默

    有的人可能奇怪，getLine已经给的是String类型了吧，不然也没法对input用那个String.trimAscii操作，怎么还要toString转化呢？这是因为那个trimAscii返回的不是String类型，而是String的一个局部引用，子视图的感觉

  6. 对input调用一个String.toNat?函数，这个函数尝试将input从String转化为Nat自然数，失败返回“none”，成功返回“some 作为结果的自然数”

    这里none和some是函数，可用于构建Option选项类型，如果你不懂Option选项类型是干什么用的，大概就是用来表示一个可以为空的东西

  7. 尝试匹配转化得到的新自然数，如果是none，说明输入的压根不是数，我们提示输入数子并重新调用自身，如果有值，那么将它与答案比较大小

    这里我们将attempts加一，这样就记录下了尝试的次数

    不知道你有没有对那个s!感到奇怪，但lean里用模板字符串就得这么写，比方说你有个String类型变量name，值是"Bob"，你可以用Std.IO.println s!"Hello, {name}!"来打印Hello, Bob!并保留一定的自由度，比方说把name的值改成"World"

  8. 最后这个main函数将作为程序入口，我们不需要它接受输入，但需要它返回任意的IO模块输出值

    函数定义末尾的do只在我们无法知道函数多久完成时需要，一般来说只要包含了Action行为就需要，这里的多久是cpu计算量而非真实时间

  9. 得到运行时程序的标准输入（一般来说是命令行），得到一个1到100间的随机数，由于默认步长为1，所以我们得到的是1、2、3、...、100中的一个，最后开始游戏并额外传递0作为已猜测次数

保存文件后用lean --run test.lean来运行，记得加上--run指令，不然lean只会执行类型检查，不会运行文件内定义的main函数。

可以试试啊，看看你要多少次才能猜对。

虽然这部分严格来说和用lean搞数学证明关系不能说不大，只能说一点没有，但是我认为用来熟悉一下lean是很有必要的。因此建议把这个脚本每行每个词在干什么弄清楚，特别是没有其它语言编程经验的，跳过这里后面没看懂也别怪我。

至于怎么弄清楚，即便我觉得每行都解释在做什么已经足够，但毕竟是我觉得，所以还是说一下。千万不要去看官方文档，这很重要，不是英语的问题，而是lean的官方文档非常垃圾，跟注水论文一桌，看了也是浪费时间，连AI都是直接看专门写的SKILL文件而不是它那些纯粹为了存在而存在的文档。不会的关键词或局部写法直接去问AI，那个partial是什么东西我就是问AI的，看到AI吐lean比吐js和python正确率还高，我是有点难绷的。

一点数学

刚才是一般编程，我们来看看形式化验证怎么写。

考虑一个红绿灯的建模，简单起见，红绿灯秒数皆为自然数，分别倒计时，按红绿黄的顺序循环。

我打算在他们上面定义加法和减法，加法增加秒数，减法减少秒数，其中只有减法会导致变灯，最后我们将考虑在给定一个红绿灯和当前状态的情况下判断几秒后或几秒前的状态。

import Std

inductive TrafficLight where
  | red (secondsLeft : Nat)
  | yellow (secondsLeft : Nat)
  | green (secondsLeft : Nat)
deriving Repr, DecidableEq

def redDefault : Nat := 20
def yellowDefault : Nat := 3
def greenDefault : Nat := 10

def addSeconds (target : TrafficLight) (n : Nat) : TrafficLight :=
  match target with
    | .red s => .red (s + n)
    | .yellow s => .yellow (s + n)
    | .green s => .green (s + n)

def minusOneSecond (target : TrafficLight) : TrafficLight :=
  match target with
    | .red s =>
      if s-1 > 0 then
        .red (s - 1)
      else
        .green greenDefault
    | .yellow s =>
      if s-1 > 0 then
        .yellow (s - 1)
      else
        .red redDefault
    | .green s =>
      if s-1 > 0 then
        .green (s - 1)
      else
        .yellow yellowDefault

def minusSeconds (target : TrafficLight) (seconds : Nat) : TrafficLight :=
  if seconds > 0 then
    minusSeconds (minusOneSecond target) (seconds-1)
  else
    target
termination_by seconds

稍微解释一下，具体关键词用法去问AI，这里主要是定义一个三状态的TrafficLight类并自动集成了用于#eval求值和比较是否相等的特性。

然后是加减秒数的实现，其中减多秒被实现为递归的减一秒，请注意它下面的被seconds变量终止声明，这明确告诉lean我们的递归是会终止的，而不是用partial告诉它请当这个函数是会终止的。虽然这里用partial也能避免报错，但是用partial会影响之后的形式化证明，因为lean并不信任可能永远不会终止的partial函数。

而且我们这里没有再写do，这是因为没有Action行为，没有副作用的纯函数不需要do。

把它保存到trafficlight.lean文本文件里。

请专门给这个文件一个文件夹，然后在新的文件夹内执行lake init来初始化一个项目。

本文不涉及如何使用lake以及lean下好的编程范式，用lake开项目只是因为我没找到其他办法让lean支持模块化，它似乎只在安装时附带的库目录找模块，只有lake环境能让我放自己写的模块进去。

用lean --o=trafficlight.olean trafficlight.lean生成一个导出文件并放到.lake/build/lib/lean里面，别问为啥要多这一步，问就是我不知道有什么更好的办法，可能这也是lean特色吧。

放好后我们这个文件夹的lake环境就可以用import trafficlight来引用我们自己的TrafficLight类了。

接下来我们在test文件夹下新建一个TrafficLight.lean并输入如下内容作为测试。

import trafficlight

def check (name : String) (actual expected : TrafficLight) : IO Unit := do
  if actual == expected then
    IO.println s!"PASS: {name}"
  else
    throw <| IO.Error.userError
      s!"FAIL: {name}; expected {repr expected}, got {repr actual}"

def runTrafficLightTests : IO Unit := do
  check    "red changes to green at zero"    (minusOneSecond (TrafficLight.red 1))    (TrafficLight.green greenDefault)
  check    "yellow changes to red at zero"   (minusOneSecond (TrafficLight.yellow 1)) (TrafficLight.red redDefault)
  check    "green changes to yellow at zero" (minusOneSecond (TrafficLight.green 1))  (TrafficLight.yellow yellowDefault)
  check    "red minusSeconds"                (minusSeconds (TrafficLight.red 5) 2)    (TrafficLight.red 3)
  check    "yellow minusSeconds to red"      (minusSeconds (TrafficLight.yellow 1) 5) (TrafficLight.red 16)
  check    "yellow addSeconds still yellow"  (addSeconds (TrafficLight.yellow 2) 8)   (TrafficLight.yellow 10)

def main : IO Unit := do
  runTrafficLightTests

你可能记得，我们建模的红绿灯红灯20秒，黄灯3秒，绿灯10秒，到0切换下一个灯，顺序依次为红、绿、黄。

中间测试的六项都到这里了总能看懂吧，可以自己试一试啊，看看是否全部PASS。

怎么试呢，保存好文件后，我们在项目文件夹下运行lake env lean --run test/TrafficLight.lean，这里的lake env很重要，在lake这个项目的环境下运行我们放到.lake/build/lib/lean/的olean文件才能被lean找到。

验证是验证了，这样的红绿灯也是“运行”起来了，但是这验证也不是形式化验证啊，这只是命令行打印信息而已。是的，还没到形式化验证，一步步来。

请冷静一下，从逻辑上说，我们是不是定义了一种带状态可转化抽象，是不是也找到办法验证我们的抽象是否真的运作，虽然我这里演示的抽象不是高大上的数学概念，验证方式也不像lean。如果你能理解或者说至少跟着从猜数字那里到这个不那么lean的验证方式，所有的命令都没有报错，行为和我这里描述相符，恭喜，其实你已经会用lean了，接下来我们看看怎么运用lean作为证明器的功能。

现在我的验证方式有什么问题，输出需要人看，全PASS表示通过对不对？这样在编程中可以接受，因为编程顶了天一个项目也就百来个自动化测试条目，毕竟程序员他不是靠单元测试数量拿工资的嘛。但是数学证明不是这样，复杂点的定理动不动就需要几千上万个检查点，还得全部通过才算成功。而且数学证明他一般前面的定理错了后面也会全错，所以压根没必要人去看有没有全PASS，研究者反正是一点点走通的，给我们证明的时候我们只关心是不是全部通过。

lean是怎么解决这个问题的呢，你要证数学，它自动给你测试，只要测试不通过，直接报错拒绝编译，这么做放在编程是灾难了，整个周末加班没编译出来一次，但是数学上是好事，研究者的代码我们检查一下他设置的条件和目标，然后直接看能不能编译，只要不报错他就是对的，连中间步骤都不用检查。

这里建议尽量完全理解前文的代码和各个命令，至少也应当跟着我的描述走一遍。

下面我们给出验证文件的形式化版本。

请新建文件TrafficLightProof.lean并输入如下内容。

import trafficlight
theorem red_changes_to_green : minusOneSecond (TrafficLight.red 1) = TrafficLight.green greenDefault := by
  decide
theorem yellow_changes_to_red : minusOneSecond (TrafficLight.yellow 1) = TrafficLight.red redDefault := by
  decide
theorem green_changes_to_yellow : minusOneSecond (TrafficLight.green 1) = TrafficLight.yellow yellowDefault := by
  decide
theorem red_minusSeconds : minusSeconds (TrafficLight.red 5) 2 = TrafficLight.red 3 := by
  simp [minusSeconds]
  decide
theorem yellow_minusSeconds_to_red : minusSeconds (TrafficLight.yellow 1) 5 = TrafficLight.red 16 := by
  simp [minusSeconds]
  decide
theorem yellow_addSeconds_still_yellow : addSeconds (TrafficLight.yellow 2) 8 = TrafficLight.yellow 10 := by
  decide

现在我们运行lake env lean TrafficLightProof.lean来看看能否成功编译，有没有报错，没有的话就是全部通过。

注意看我这里的红绿灯六大定理，其实挺像函数定义的，只不过变成了 theorem 定理名 定理内容 证明内容。

定理内容不一定要是等式，任何能表述成“某某事情真”或“某某事情假”的事情都可以是定理内容，证明内容是怎么回事呢，我们需要一系列Tactic策略，比如我这里decide能解决纯函数代入的式子，但遇到minusSeconds这种递归操作就傻眼了，我们用simp化简策略先把lean确信可以终止的minusSeconds交给它。

你可以试试把其中一个simp [minusSeconds]或者下一行的decide去掉会发生什么，这非常重要，这是用lean作为证明器来用的关键之一，一定要自己试一下，看看lean程序打印出什么东西。这里我就故意省略了免得有人当故事读没学会还怀疑我藏了宝，从猜数字那里就没跟的傻眼了吧，还没完，这里的代码我是不作为项目的，只在这个博客里出现，我这里测完就删了，没有现成的提供。

Mathlib

把红绿灯定理放在一边，完全明白怎么回事后再抱着看“红灯之后是绿灯”，真是梦回幼年了。

让我们要看看怎么用Mathlib，实际一点。

先在lakefile.toml里加一块，写明Mathlib依赖，像下面这样。

[[require]]
name = "mathlib"
scope = "leanprover-community"

接下来运行lake update，然后等，它会从Github下载相关仓库。

最后是可选的lake exe cache get。

值得注意的是我没有成功，因为编译失败，所以这三步正确性我无法验证。我真是头一次见装个插件之类的东西都需要在用户设备上编译的语言，无语了。

也就是说我无法安装Mathlib，安装后的效果就是你可以import Mathlib之类的。

接下来我用网页版大致说一下代码上怎么用Mathlib，安装这块真的没折。

这里主要是AI的使用，因为Mathlib的文档和没有一样，真不愧是lean下的项目，我怀疑这些贡献Mathlib的研究员全是拿AI来Vibe Coding的，Mathlib在Github仓库的维基页面居然一直在讲如何从老lean版本过渡过来之类的，我就不明白了，这和Mathlib有啥关系。

所以不要想着去学Mathlib怎么用啊，这玩意不像人类写的，也明显不是给人类学的，lean上的数学就是EvE比赛，人类唯一的参与就是看一下theorem是什么，然后等AI尝试直到编译成功。

看到这里的可能要赚了，我这人很少谈提示词，也不感兴趣，这次是教程刚好写到这份上了，我想着还是让教程完整一点吧。虽然依然不会涵盖elan啊lake啊之类的工具怎么用，但我先前已经说了要教Mathlib，言而无信非君子，AI就AI吧。

不过，在那之前我们回忆一下到底是什么在阻碍我们使用Mathlib，是我们不会用lean编程吗，不是的，能理解猜数字就不是这个问题，是我们不知道怎么使用附加模块吗，不是的，我们的红绿灯定义就是项目内的额外模块，是我们不知道怎么用lean形式化证明定理吗，不是的，最后我们也成功将基于打印信息的验证改写为只要编译成功就等于全部通过的形式化定理了。

那么，到底是哪里缺了？我们不知道Mathlib提供了什么，准确的说，不知道import Mathlib后会得到什么。

在红绿灯定理的证明中，我们import trafficlight后为什么能清楚的知道里面有TrafficLight类，有minusSeconds之类的函数，有三个默认值，甚至知道类包含项目以及函数需要的参数？因为这是我手打的，简短且解释的很清楚的源码摆在旁边。Mathlib不是这样，我们不知道它能提供什么，变量名、函数名、函数期待的参数和返回值、一些策略、定理统统没有，而我们又没有办法去翻源码，因为人类是无法看懂它的源码的，好吧，其实是很难看懂而已。

我们能做的，只有问AI，就问有什么策略，什么定理之类的，以及去看它项目的目录结构，不要点进去看源代码，但看目录结构有好处。

现在到浏览器打开我们关心的目录，import Mathlib就是会把这个目录下所有东西引入。

有的目录或文件名很清楚的表明了它是关于什么的，按数学分的类，有的就不是，比如Basic，什么叫基本呢？

点进去并翻到最下面看README，这种README得看，而且README用AI写的非常少见。它说Basic这里包含的是很多数学领域都需要的定义。

比方说，我现在想形式化的证明一个N×N（也就是形如x，y的数组集合，x、y都是自然数）可数。

可数，Basic里面就有个Countable，很明显得用上。然后呢，只有Countable应该不够，集合和自然数未必包含在这个可数文件夹里，是外面的NumberTheory文件夹吗，还是什么？

于是，问AI“使用lean4 mathlib，形式化的证明一个N×N（也就是形如x，y的数组集合，x、y都是自然数）可数，除了Mathlib.Basic.Countable，还需要引入什么模块？”。

没想到AI回答不需要，因为这东西在Mathlib.Basic.Countable.Basic中已经包含了，我便拿着它给的短例去Mathlib/Basic/Countable/Basic.lean的源代码页面查找，确实包含了，相关片段如下。

instance [Countable α] [Countable β] : Countable (α × β) := by
  rcases exists_injective_nat α with ⟨f, hf⟩
  rcases exists_injective_nat β with ⟨g, hg⟩
  exact (Nat.pairEquiv.injective.comp <| hf.prodMap hg).countable

instance [Uncountable α] [Nonempty β] : Uncountable (α × β) := by
  inhabit β
  exact (Prod.mk_left_injective default).uncountable

instance [Nonempty α] [Uncountable β] : Uncountable (α × β) := by
  inhabit α
  exact (Prod.mk_right_injective default).uncountable

既然它已经被证明过了，我们需要做的就是理解它怎么做的。怎么理解呢，就是把这段发给AI并让AI解释，每个策略在干什么，每个函数或行为做了什么。永远不要试图自己看源代码，翻源代码唯一目的就是找出AI声称存在某内容的相关代码并还给AI要解释，也不要想着这rcases啊inhabit啊exact啊不懂做什么的去文档找，直接问AI。

而Mathlib为了使用方便，import Mathlib会把Mathlib所有提供的东西都导入，所以下面的代码可以正常编译，也就是正确。

import Mathlib

example : Countable (ℕ × ℕ × ℕ) := by
  infer_instance

这里的example和theorem没有区别，好吧，example没有定理名，类似国内写证明的“引理123”。或许红绿灯定理应该用example，变成匿名的红绿灯引理。

懂了吧，但别急，还有一点没有说，那就是数学不可能一直在验证早被证明正确的东西，比方说ℕ × ℕ × ℕ × ℕ还没有被证明可不可数，岂不是没法玩了？因为lean只保证能成功编译必然正确，不能保证编译报错必然错误啊！

这个也简单，可以先试一试嘛，看看现有的策略之类的能不能推出ℕ × ℕ × ℕ × ℕ可不可数。

import Mathlib

#synth Countable (ℕ × ℕ × ℕ × ℕ)

这里我们把“ℕ × ℕ × ℕ × ℕ是Countable可数”的这一Prop命题传递给#synth指令，可以看到它返回了一个缩写的实例名，说明找到一个证明了，也就是命题是真的。

这个查找也可以用本来只能检查类型的#check指令实现，换成#check (inferInstance : Countable (ℕ × ℕ × ℕ × ℕ))试一试吧。

你可能奇怪，正确了也没明确提示啊，是的，因为错误的话就直接报错中断了，所以你没看到错误就是对的。

后记

这次简介就到这里吧，有挺多东西没有涉及到，但我感觉也没有必要，万事开头难，希望这篇博客能帮想用lean的人开个头。

lean一般需要的功能本文都有涉及，除了elan和lake的具体使用。

后记这里解释一下为什么不谈elan、lake，而且整篇教程一直是给点代码，解释一点，最后直接描述了一波Vibe Coding。

不谈elan、lake的主要原因是我的电脑环境下使用lean并不方便，VSCode什么的根本用不了，elan这种需要你执行他脚本的也用不了，只能装一个裸lean4，还好lake是包含在lean4里面的。给点代码解释一点是因为这样最好跟也最好理解，你读一读，不懂的关键词问问AI，在自己电脑上按我描述跑一跑就差不多明白了。最后学用Mathlib需要AI帮是不得已，它就是设计给AI看的，即便是人写，也是为了AI写的，不信你去看看Mathlib主页宗旨就明白了，AI吃点标注数据就学会了，人可吃不进去标注图和权重表啊。

还有，这玩意到底能不能用来编程，当函数式语言用，理论上图灵完备的语言都可以，但没有人会拿brainfuck写任何有用的东西，就算你接触过Haskell乃至Prolog，编程这活也轮不到lean。从编程角度来说，光是lean既要各种奇怪符号，又要保证缩进正确，就已经输了。不过，未来也可能有为了搞数学学lean的人走向程序且懒得换语言，Nodejs不就是这么来的嘛。所以在我看来lean是不能用于编程的，数学研究者当它是个可被AI驱动的形式化证明器就够了。

至于能抽象证数学的语言很多，怎么就lean出名呢，因为只有lean能方便的对接AI，懂了吧。

我不知道有没有人期待教程包含怎么把lean对接AI，来自动证明或者构造的，那样的话得辜负期待了。简单来说就是让Agent拿着一个lean repl玩，这个repl原生不支持，且用的格式是JSON，就是为对接AI弄的，需要用额外的模块来模拟。具体一步步的怎么做我不清楚。我只是把AI当自然语言网站黄页用的，不懂AI训练、微调、接口那些事情。AI Agent我是完全没有使用过的，所以我连怎么让LLM收发JSON都不知道。