LEAN 简介

GlimpseOfLean 项目的非官方文档，旨在为初学者提供一个快速入门指南。

这个仓库是为想快速了解 LEAN 的人提供一个入门介绍。目标是在2到3个小时内了解在 LEAN 中进行证明的样子。 阅读 Introduction.lean 文件后，您应该阅读 Basics 文件夹中的解释和练习，并选择从 Topics 文件夹中的一个文件开始工作。当然，如果您有更多时间，您可以尝试该文件夹中的所有文件。

要使用 LEAN 进行工作，您可以在本地安装 LEAN，使用 Codespaces 或使用 Gitpod。

  • 要使用 Codespaces，请确保已登录 Github，点击下面的按钮，选择 4-core，然后按下 Create codespace。几分钟后，一个带有 LEAN 的编辑器将在您的浏览器中打开。

Open in GitHub Codespaces

  • Gitpod与 Codespaces 非常相似，请点击下面的按钮，按下 Continue 并等待几分钟。

Open in Gitpod

  • 要在本地安装 LEAN，请按照这里的说明进行操作。

如果您有更多时间，您还应阅读《LEAN中的数学》一书（链接）。