Lean 中文文档¶

Lean 简介¶

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

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

相关资源¶

翻译及教程¶

• Lean4 安装及 Lake 环境管理
• Lean4 语言初探
• Lean4 函数式编程
• Lean4 定理证明
• Lean4 自然数游戏
• Lean4 游戏教程
• LeanDojo 使用教程

进行中¶

• GlimpseGame 定理证明游戏的制作及翻译
• Lake 文档翻译

计划中¶

• Lean 形式化数学：Mathematics in Lean
• LeanCopliot，LLMStep 等工具教程及实现机制
• ...

相关推荐¶

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

联系我们¶

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