Lean 教程(二) ｜ 函数式编程

发表于 更新于 阅读次数： 字数： 512 时间 ≈ 2 分钟
学习 Lean 的途径很多，具体取决于你的背景和偏好，这些教程有偏重数学的也有偏重编程的。

教程定位

学习 Lean 的教程和途径很多，具体取决于个人知识背景和偏好。这些教程里，有偏重数学的也有偏重编程的。

快速上手

  1. 自然数游戏 NNG4，在线交互式 Lean 教程，重点是证明自然数基本运算的属性。 Lean Game Server 托管各种学习游戏，包括集合论、逻辑和 Robo（一个关于本科数学的故事）等。

  2. 快速上手的 Lean 初探教程，涵盖使用 Lean 证明的一些基本概念，也包括初级分析、抽象拓扑和数理逻辑的独立主题。

  3. 如果希望直接从源代码学习， Lean API 文档 不仅包括 Mathlib ，还包括 Std、 Batteries、Lake 和核心编译器，这是最接近现有综合参考手册的内容。

文档教程

  1. 数学导向的 Mathematics in Lean，以及节奏更缓的 The Mechanics of Proof

  2. 从类型论基础出发的 Theorem Proving in Lean，计算机科学导向的 The Hitchhiker’s Guide to Logical Verification

  3. 侧重将 Lean 作为编程语言的 Functional Programming in Lean 以及侧重元编程策略编写的 Metaprogramming in Lean

  4. 更关注 LEAN 本身而不仅是使用的 Reference manual

系列定位

教程系列从 LEAN 函数式编程切入，在文档基础上，加上个人的理解和精炼。主要参考 Theorem Proving in Lean，目前也有社区翻译版 fp-lean-zh。

该书面向的场景：使用 LEAN 作为证明助手的数学家在某些时候可能需要编写自己的证明自动化工具。随着工具变得越来越复杂，它们开始类似于函数式语言的程序，不过多数数学家都接受过 Python 和 Mathematica 等语言的培训。这本书可以帮助弥合差距，使更多的数学家能够编写可维护和易于理解的证明自动化工具。

本地安装 Lean 的方式参看上一篇，也可以通过 live.lean-lang.org 或 live.leanprover.cn 在线使用。