Lean 中文文档¶
Lean 是什么¶
Lean 是微软研究院在 2013 年推出的计算机定理证明器。Lean4 于 2021 年发布，为 Lean 定理证明器的重新实现，能够生成 C 代码后进行编译，以便开发高效的特定领域自动化。
Lean 作为一门独特的语言，兼具 数学和编程 两方面的特性。
- 作为交互式定理证明器，Lean 提供了严格的逻辑框架，数学家可以将数学定理转换成代码，并严格验证这些定理的正确性。
- 作为通用函数式编程语言，它具有 依赖类型 的 严格 的 纯函数式 语言性质。
这些特性让 Lean 在数学和计算机科学研究中非常有用，它可以帮助研究人员发现并纠正概念上的错误，同时加深他们对研究对象的理解。Lean 的标准库 mathlib 被称为未来的数学图书馆。
关于 Lean-zh¶
Lean-zh 是一个自发组成的团体，旨在推动 Lean 在中文学术和编程社区的普及和应用。
Lean-zh 提供了一个学习与实践的平台，如果你对 Lean 感兴趣，无论是参与编写 Lean 教程、翻译官方文档、开发 Lean 项目，还是以其他方式贡献力量，欢迎你的加入！
快速上手¶
学习 Lean 的教程和途径很多，具体取决于个人的知识背景和偏好。这些教程有偏数学的也有偏编程的。
数学方面：
- 自然数游戏 NNG4：在线交互式 Lean 教程，重点在证明自然数基本运算的属性。此外，Lean Game Server 托管各种学习游戏，包括集合论、逻辑和 Robo（一个关于本科数学的故事）等。
- 快速上手的 Lean 初探教程：涵盖使用 Lean 证明的一些基本概念，也包括初级分析、初等数论和数理逻辑的独立主题。
编程方面：可以浏览网站顶部的其他标签，包括与 Lean 交互的常用编程工具和 Lean 项目教程等，教程干货正在路上。。。
Lean-zh 译制¶
目前 Lean-zh 已翻译的资源：
- Lean4 函数式编程（Functional Programming in Lean）
- Lean4 定理证明（Theorem Proving in Lean）
- Lean4 元编程（Metaprogramming in Lean）
进行中
- Lean 形式化数学(Mathematics in Lean)
- Lean 交互工具和实用项目的教程介绍
计划进行
- GlimpseToGame 定理证明游戏制作及翻译
- Tactic 手册及如何编写 tactic
- LeanCopliot，LLMStep 等实用工具教程及实现机制
- ...
联系我们¶
如果有任何问题、建议或想参与到社区中来，欢迎加入 QQ 群 897971266 或 Telegram 讨论组 来一起交流。
其他资源¶
数学导向：
- 经典教材 Mathematics in Lean
- 节奏更缓的 The Mechanics of Proof
- 从类型论基础出发的 Theorem Proving in Lean
计算机导向：
- 侧重将 Lean 作为编程语言的 Functional Programming in Lean
- 侧重元编程策略编写的 Metaprogramming in Lean
- 更关注 LEAN 本身而不仅是使用的 Reference manual
- 计算机科学角度的 The Hitchhiker's Guide to Logical Verification
其他推荐：