Merge pull request #10 from Lean-zh/rex/update-homepage

update tutorials

Author: RexWzh

docs/index.md

@@ -20,59 +20,75 @@ description: Lean-zh Documentation
   </a>
 </div>
 
+## Lean 是什么
 
-## Lean 简介
+Lean 是微软研究院在 2013 年推出的计算机定理证明器。Lean4 于 2021 年发布，为 Lean 定理证明器的重新实现，能够生成 C 代码后进行编译，以便开发高效的特定领域自动化。
 
-Lean 是一个交互式定理证明器（Interactive Theorem Prover, ITP），也是一门通用函数式编程语言。微软研究院在 2013 年推出这一计算机定理证明器，数学家可以把数学定理转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。当被视为编程语言时，Lean 是一种具有 **依赖类型** 的 **严格** 的 **纯函数式** 语言(strict pure functional with dependent types)。
+Lean 作为一门独特的语言，兼具 **数学和编程** 两方面的特性。
 
-在形式化方面，Lean 提供了一套严格的逻辑和数学框架，使得用户可以进行精确的推理和证明。这个特性使得 Lean 在数学和计算机科学研究中非常有用，它可以帮助研究人员发现和改正概念上的错误，同时也让他们能够更深入地理解其研究主题。
-很多数学家选择使用 Lean 的标准库 mathlib 作为基础，这个仓库被称为[未来的数学图书馆](https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/)。
+- 作为交互式定理证明器，Lean 提供了严格的逻辑框架，**数学家可以将数学定理转换成代码，并严格验证这些定理的正确性**。
+- 作为通用函数式编程语言，它具有 **依赖类型** 的 **严格** 的 **纯函数式** 语言性质。
 
-## Lean-zh
+这些特性让 Lean 在数学和计算机科学研究中非常有用，它可以帮助研究人员发现并纠正概念上的错误，同时加深他们对研究对象的理解。Lean 的标准库 [mathlib](https://github.com/leanprover-community/mathlib4) 被称为[未来的数学图书馆](https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/)。
+
+## 关于 Lean-zh
 
 Lean-zh 是一个自发组成的团体，旨在推动 Lean 在中文学术和编程社区的普及和应用。
 
-如果你对 Lean 感兴趣，对编写 Lean 教程、翻译官方文档、开发 Lean 项目，或者任何其他形式的贡献感兴趣，欢迎加入我们。
+Lean-zh 提供了一个学习与实践的平台，如果你对 Lean 感兴趣，无论是参与编写 Lean 教程、翻译官方文档、开发 Lean 项目，还是以其他方式贡献力量，欢迎你的加入！
+
+### 快速上手
 
+学习 Lean 的教程和途径很多，具体取决于个人的知识背景和偏好。这些教程有偏数学的也有偏编程的。
 
-## 相关工作
+**数学方面**：
 
-### Lean4 教程
+1. 自然数游戏 [NNG4](https://nng4.leanprover.cn)：在线交互式 Lean 教程，重点在证明自然数基本运算的属性。此外，Lean Game Server 托管各种学习游戏，包括集合论、逻辑和 Robo（一个关于本科数学的故事）等。
+2. 快速上手的[ Lean 初探教程](https://github.com/Lean-zh/GlimpseOfLean)：涵盖使用 Lean 证明的一些基本概念，也包括初级分析、初等数论和数理逻辑的独立主题。
 
-  * [Lean4 安装教程](tutorial/install.md)
-  * [Lean4Game 游戏编写教程](tutorial/lean4game.md)
-  * [LeanDojo 使用教程](tutorial/lean-dojo.md)
+**编程方面**：可以浏览网站顶部的其他标签，包括与 Lean 交互的常用编程工具和 Lean 项目教程等，教程干货正在路上。。。
 
-### 文档翻译
+### Lean-zh 译制
 
-  - <a href="https://www.leanprover.cn/GlimpseOfLean/" target="_blank"> Lean4 语言初探 <i class="fas fa-external-link-alt"></i></a>
-  - <a href="https://www.leanprover.cn/fp-lean-zh/" target="_blank"> Lean4 函数式编程 <i class="fas fa-external-link-alt"></i></a>
-  - <a href="https://www.leanprover.cn/tp-lean-zh/" target="_blank">Lean4 定理证明 <i class="fas fa-external-link-alt"></i> </a>
-  - <a href="https://game.leanprover.cn/#/g/local/NNG4" target="_blank"> Lean4 自然数游戏 <i class="fas fa-external-link-alt"></i></a>
-  - <a href="https://www.leanprover.cn/mp-lean-zh/" target="_blank">Lean4 元编程 <i class="fas fa-external-link-alt"></i> </a>
+目前 Lean-zh 已翻译的资源：
 
-### 进行中
+- [Lean4 函数式编程（Functional Programming in Lean）](https://www.leanprover.cn/fp-lean-zh/)
+- [Lean4 定理证明（Theorem Proving in Lean）](https://www.leanprover.cn/tp-lean-zh/)
+- [Lean4 元编程（Metaprogramming in Lean）](https://www.leanprover.cn/mp-lean-zh/)
 
-  * [GlimpseToGame 定理证明游戏的制作及翻译](https://github.com/Lean-zh/GlimpseGame)
-  * [Lean 形式化数学](https://www.leanprover.cn/math-in-lean-zh/)
+**进行中**
 
-### 计划中
-  * Tactic手册及如何编写tactic
-  * LeanCopliot，LLMStep 等工具教程及实现机制
-  * ...
+* [Lean 形式化数学(Mathematics in Lean)](https://www.leanprover.cn/math-in-lean-zh/)
+* Lean 交互工具和实用项目的教程介绍
 
-### 相关推荐
+**计划进行**
 
-  * 软件基础：[Software Foundations](https://coq-zh.github.io/SF-zh/)
-  * [编程语言基础：Agda 描述](https://agda-zh.github.io/PLFA-zh/)
+* [GlimpseToGame 定理证明游戏制作及翻译](https://github.com/Lean-zh/GlimpseToGame)
+* Tactic 手册及如何编写 tactic
+* LeanCopliot，LLMStep 等实用工具教程及实现机制
+* ...
 
-## 其他链接
-  
-  * Lean-zh 官网: https://leanprover.cn
-  * Lean 社区官网: https://lean-lang.org
-  * Lean 的 Zulip 社区: https://leanprover.zulipchat.com
-  * 自然数游戏: https://nng4.leanprover.cn
 
-## 联系我们
+### 联系我们
 
 如果有任何问题、建议或想参与到社区中来，欢迎加入 QQ 群 897971266 或 Telegram [讨论组](https://t.me/Lean_zh_CN) 来一起交流。
+
+## 其他资源
+
+**数学导向**：
+
+  - 经典教材 [Mathematics in Lean](https://leanprover-community.github.io/mathematics_in_lean/)
+  - 节奏更缓的 [The Mechanics of Proof](https://hrmacbeth.github.io/math2001/)
+  - 从类型论基础出发的 [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html)
+
+**计算机导向**：
+
+  - 侧重将 Lean 作为编程语言的 [Functional Programming in Lean](https://leanprover.github.io/functional_programming_in_lean/)
+  - 侧重元编程策略编写的 [Metaprogramming in Lean](https://github.com/arthurpaulino/lean4-metaprogramming-book)
+  - 更关注 LEAN 本身而不仅是使用的 [Reference manual](https://leanprover.github.io/lean4/doc/)
+  - 计算机科学角度的 [The Hitchhiker's Guide to Logical Verification](https://raw.githubusercontent.com/blanchette/logical_verification_2023/main/hitchhikers_guide.pdf)
+
+**其他推荐**：
+
+* 软件基础：[Software Foundations](https://coq-zh.github.io/SF-zh/)
+* [编程语言基础：Agda 描述](https://agda-zh.github.io/PLFA-zh/)

docs/install.md

@@ -0,0 +1,107 @@
+# LEAN 4 安装教程 
+
+Lean 4 工作环境由以下几部分组成：
+
+1. [elan](https://github.com/leanprover/elan)：Lean 版本管理器。功能类似于 Rust 的 `rustup` 或 Node.js 的 `nvm`，用于安装、管理和切换不同版本的 Lean。
+2. [lake](https://github.com/leanprover/lake)：Lean 的包管理器，全称 Lean Make，已合并为 Lean 4 仓库源码的一部分。用于创建 Lean 项目，构建 Lean 包，配置 Mathlib 和编译 Lean 可执行文件。
+3. （非必须）[Mathlib](https://leanprover-community.github.io/mathlib4_docs/)：Lean 的数学库。
+
+为了使用 Lean，你需要先安装 [VS Code](https://code.visualstudio.com/) 和 Git，然后安装 elan，elan 会自动帮你安装 Lean 4 stable 以及 lake 包管理器，接下来就可以使用 lake 创建自己的 Lean 项目。
+
+> 如果希望快速了解和使用 Lean，除了在本地安装，也可以通过 [live.lean-lang.org](https://live.lean-lang.org) 或 [live.leanprover.cn](https://live.leanprover.cn) 在线体验。
+
+## Linux 安装 elan
+
+以下内容在 Ubuntu 22.04 系统上测试通过。
+
+如果没有网络问题，用一行命令安装：
+
+```bash
+wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
+```
+
+脚本执行内容包括：检查并安装 VsCode，Lean 插件以及 elan。
+
+如果访问 GitHub 存在问题，可以在安装 vscode 后，手动安装 elan。
+
+具体地，在 GitHub [release 页面](https://github.com/leanprover/elan/releases)或者 [上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html) ，根据系统版本下载 elan。
+
+比如下载 `linux-x86_64` 系统的 elan 工具：
+
+```bash
+# 如果网络不行就本地下载再上传
+curl -L https://github.com/leanprover/elan/releases/download/v3.1.1/elan-x86_64-unknown-linux-gnu.tar.gz -o elan.tar.gz
+tar xf elan.tar.gz
+```
+
+解压得到 `elan-init` 文件，赋予可执行权限并执行安装：
+
+```bash
+chmod +x elan-init
+./elan-init -y --default-toolchain none
+```
+
+默认安装最新版本的 Lean，也可以通过参数指定版本，或略过具体 Lean 版本的安装。
+
+完成后，在 `.bashrc` 或 `.zshrc` 中修改环境变量：
+
+```bash
+export PATH="$HOME/.elan/bin:$PATH"
+```
+
+重启终端，检查 `elan` 版本和默认安装的 Lean 版本：
+
+```bash
+❯ elan -V
+elan 3.1.1 (71ddc6633 2024-02-22)
+❯ elan show
+stable (default)
+Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
+```
+
+## Windows 安装 elan
+
+先在这里下载安装 [VS Code](https://code.visualstudio.com/download) 和 [Git](https://gitforwindows.org/)。
+
+安装 VS Code 后，需要安装 lean4 扩展（extension）。如果网络环境顺畅，可以在 lean4 扩展的欢迎页选择 Get Start 来完成安装，或者创建空的 Lean 文件时扩展会弹出提示提醒你安装 elan 和 Lean 4。
+除了这种方式，也可以在 cmd 或 powershell 中运行命令
+
+```
+curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
+powershell -ExecutionPolicy Bypass -f elan-init.ps1
+del elan-init.ps1
+```
+
+如果遇到了 `"SSL connect error", "Timeout was reached","Failed to connect to github.com port 443"...` 等错误，就是说明你的网络环境不理想。如果这样可以通过[上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html)安装。下面演示在网络环境不理想的条件下的安装。
+
+打开 cmd 或 Powershell，运行
+```
+curl -O --location https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/elan/releases/download/eager-resolution-v5/elan-x86_64-pc-windows-msvc.zip
+unzip -o elan-x86_64-pc-windows-msvc.zip
+.\elan-init.exe
+```
+会在终端中开始安装程序。单击回车在默认位置 `~\.elan` 安装。
+
+安装完成后可以删除刚刚下载的临时文件：
+
+```
+del elan-init.exe
+del elan-x86_64-pc-windows-msvc.zip
+```
+
+添加 elan 的安装地址到 PATH 环境变量（如果是默认安装，那么是 `%USERPROFILE%\.elan\bin`）。
+
+重启终端输入 `elan --version`，如果能正常输出版本号，那么你已经装好了 elan 和 Lean 4 stable 版本。
+
+
+## Mac 安装 elan
+
+和 ubuntu 系统类似，用脚本一键安装：
+
+```bash
+/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh)" && source ~/.profile
+```
+
+或者在 GitHub [release 页面](https://github.com/leanprover/elan/releases) 或 [上交镜像源](https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html) 手动下载运行安装程序。
+
+此外，不鼓励使用 homebrew 安装 elan-init 包，这可能会落后于官方版本的更新。

docs/tutorial/elan-lake.md

@@ -0,0 +1,155 @@
+# elan 及 Lake 用法示例
+
+## elan 常用功能
+
+[elan](https://github.com/leanprover/elan) 是 Lean 环境版本管理器，用于安装、管理和切换不同版本的 Lean。
+
+```bash
+elan --version   # 输出版本号来测试安装是否成功
+elan self update # 更新 elan
+elan show        # 显示已安装的 Lean 版本
+
+# 切换默认的 Lean 版本，例如 leanprover/lean4:v4.11.0-rc1 
+# stable 是最新稳定版本，所有版本可见 https://github.com/leanprover/lean4/releases
+elan default leanprover/lean4:stable 
+
+# 也可设置，只在当前目录下使用的 Lean 版本
+elan override set leanprover/lean4:stable
+```
+
+elan 在 Windows 下的管理目录为 `%USERPROFILE%\.elan\bin`，在 Linux 下的管理目录为 `$HOME/.elan`，内容形如
+
+```bash
+❯ tree .elan -L 2
+.elan
+├── bin
+│   ├── elan
+│   ├── lake
+│   ├── lean
+│   ├── leanc
+│   ├── leanchecker
+│   ├── leanmake
+│   └── leanpkg
+├── env
+├── settings.toml
+├── tmp
+├── toolchains
+│   └── stable
+└── update-hashes
+    └── stable
+```
+
+文件说明：
+
+- `toolchains` 存放下载的各个 Lean 版本
+- `settings.toml` 是 elan 的配置文件。
+- `bin` 存放常用的二进制文件，比如 `lake`。
+
+## 通过 Lake 创建 Lean 项目
+
+对创建 Lean 项目的详细介绍参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。此处演示最基本的用法。
+
+[lake](https://github.com/leanprover/lake) 全称 Lean Make，是 Lean 4 的包管理器，用于创建 Lean 项目，构建 Lean 包和编译 Lean 可执行文件。
+
+在终端中运行（`your_project_name` 替换为你自己起的名字）
+
+```bash
+lake new your_project_name
+
+# 或者手动创建一个新文件夹并在原地建立项目
+mkdir your_folder_name && cd your_folder_name && lake init your_project_name
+```
+
+以创建一个名为 `your_project_name` 的空白新项目。这个项目的内容形如
+
+```bash
+your_project_name
+├── YourProjectName
+│   └── Basic.lean
+├── lakefile.lean
+├── lean-toolchain
+├── Main.lean
+├── YourProjectName.lean
+└── ...
+```
+
+其中 `lakefile.lean` 是当前项目的配置文件，`lean-toolchain` 是当前项目使用的 Lean 版本。其他文件的功能以及更多细节请参考[这个教程](https://www.leanprover.cn/fp-lean-zh/hello-world/starting-a-project.html)。
+
+初次让 Lean Server 运行该项目时会添加
+
+```bash
+├── .lake
+   ├── lakefile.olean.trace
+   └── ...
+├── lake-manifest.json
+```
+
+如果你想在这个现有的工程中引用 Mathlib4，你需要在 `lakefile.lean` 文件尾中加入
+
+```bash
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4"
+```
+
+保存文件后 VS code 会提示 "Restart Lean"，点不点都没关系。
+
+下面要下载 Mathlib，注意让终端路径在你的项目文件夹下。如果你的网络情况好，那么在终端中运行
+
+```bash
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
+lake update
+```
+
+保存运行缓存会让每次编译节省一两个小时，但它当然也不是必须的：
+
+```bash
+lake exe cache get
+```
+
+否则（会相当艰难），参考[这个解决方案](https://zhuanlan.zhihu.com/p/680690436)。（不保证该参考方案的可靠性）
+
+如果你看到终端中显示了类似如下的提示：
+
+```bash
+Decompressing 1234 file(s)
+unpacked in 12345 ms
+```
+
+同时你的项目文件夹中出现了 `.lake\packages` 文件夹，那么证明你安装 Mathlib 成功了，此时 "Restart Lean" 即可使用。**注意：你要在项目所在的目录中运行 VS code，才能让 Lean 使用Mathlib。**
+
+这里提供一个实例来测试你的安装：
+
+```bash
+import Mathlib.Data.Real.Basic
+example (a b : ℝ) : a * b = b * a := by
+  rw [mul_comm a b]
+```
+
+如果你的 Lean infoview 没有任何报错，并且光标放在文件最后一行时会提示 "No goals"，证明你的 Mathlib 已经正确安装了。
+
+如果你想更新 Mathlib，在终端中运行
+
+```bash
+curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
+lake update
+lake exe cache get
+```
+
+*关于 Mathlib 的更多内容请参考 [Mathlib Wiki](https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency)*
+
+lake 的其他常用功能：
+
+```bash
+# 构建项目可执行文件
+lake build
+# 运行
+lake exec hello # Hello, world!
+# 清理构建文件
+lake clean
+# 更新依赖
+lake update
+# 运行 lakefile.lean 的脚本
+lake run <script>
+```
+
+关于 Lake 的更多用法可参考 [lake 文档](../references/lake-doc.md)。