Lean 中文文档¶

Lean 简介¶

Lean 是一个交互式定理证明器（Interactive Theorem Prover, ITP），也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。当被视为编程语言时，Lean 是一种具有 依赖类型 的 严格 的 纯函数式 语言(strict pure functional with dependent types)。

在形式化方面，Lean 提供了一套严格的逻辑和数学框架，使得用户可以进行精确的推理和证明。这个特性使得 Lean 在数学和计算机科学研究中非常有用，它可以帮助研究人员发现和改正概念上的错误，同时也让他们能够更深入地理解其研究主题。 很多数学家选择使用 Lean 的标准库 mathlib 作为基础，这个仓库被称为未来的数学图书馆。

Lean-zh¶

Lean-zh 是一个自发组成的团体，旨在推动 Lean 在中文学术和编程社区的普及和应用。

如果你对 Lean 感兴趣，对编写 Lean 教程、翻译官方文档、开发 Lean 项目，或者任何其他形式的贡献感兴趣，欢迎加入我们。

相关工作¶

Lean4 教程¶

• Lean4 安装教程
• Lean4Game 游戏编写教程
• LeanDojo 使用教程

文档翻译¶

• Lean4 语言初探
• Lean4 函数式编程
• Lean4 定理证明
• Lean4 自然数游戏
• Lean4 元编程

进行中¶

• GlimpseToGame 定理证明游戏的制作及翻译
• Lean 形式化数学

计划中¶

• Tactic手册及如何编写tactic
• LeanCopliot，LLMStep 等工具教程及实现机制
• ...

相关推荐¶

• 软件基础：Software Foundations
• 编程语言基础：Agda 描述

其他链接¶

• Lean-zh 官网: https://leanprover.cn
• Lean 社区官网: https://lean-lang.org
• Lean 的 Zulip 社区: https://leanprover.zulipchat.com
• 自然数游戏: https://nng4.leanprover.cn

联系我们¶

如果有任何问题、建议或想参与到社区中来，欢迎加入 QQ 群 897971266 或 Telegram 讨论组 来一起交流。