编辑“︁Lean安装与环境配置”︁（章节）

= Lean安装与环境配置 =

'''Lean安装与环境配置'''是学习Lean定理证明器的第一步。本节将详细介绍如何在不同的操作系统上安装Lean，并配置开发环境，以便初学者和高级用户都能顺利开始使用Lean进行形式化验证和数学证明。

== 简介 ==

Lean是一个功能强大的交互式定理证明器和函数式编程语言，由微软研究院开发。它支持数学定理的形式化验证，并广泛应用于计算机科学和数学领域。要开始使用Lean，首先需要正确安装Lean及其相关工具，并配置一个适合的开发环境。

== 安装Lean ==

Lean可以在Windows、macOS和Linux系统上安装。以下是不同平台上的安装方法。

=== Windows ===

1. 下载并安装'''Windows Subsystem for Linux (WSL)'''（推荐使用Ubuntu发行版）：
   * 打开PowerShell（管理员权限），运行以下命令：
     <syntaxhighlight lang="powershell">
     wsl --install
     </syntaxhighlight>
   * 重启计算机后，WSL将自动安装Ubuntu。

2. 在WSL中安装Lean：
   * 打开Ubuntu终端，运行以下命令：
     <syntaxhighlight lang="bash">
     sudo apt update
     sudo apt install lean
     </syntaxhighlight>

=== macOS ===

1. 使用Homebrew安装Lean：
   * 如果未安装Homebrew，先运行以下命令：
     <syntaxhighlight lang="bash">
     /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
     </syntaxhighlight>
   * 安装Lean：
     <syntaxhighlight lang="bash">
     brew install lean
     </syntaxhighlight>

=== Linux ===

1. 在基于Debian的系统（如Ubuntu）上，使用APT安装：
   <syntaxhighlight lang="bash">
   sudo apt update
   sudo apt install lean
   </syntaxhighlight>

2. 在基于Arch的系统上，使用Pacman安装：
   <syntaxhighlight lang="bash">
   sudo pacman -S lean
   </syntaxhighlight>

== 配置开发环境 ==

Lean的开发通常需要一个代码编辑器或集成开发环境（IDE）。推荐使用'''Visual Studio Code (VS Code)'''配合'''Lean 4扩展'''。

=== 安装VS Code和Lean扩展 ===

1. 下载并安装[VS Code](https://code.visualstudio.com/)。
2. 打开VS Code，安装'''Lean 4'''扩展：
   * 按<code>Ctrl+Shift+X</code>（Windows/Linux）或<code>Cmd+Shift+X</code>（macOS）打开扩展市场。
   * 搜索“Lean 4”并安装。

=== 创建Lean项目 ===

1. 新建一个文件夹作为项目目录。
2. 在项目目录中创建一个Lean文件（例如<code>Main.lean</code>），并写入以下代码：
   <syntaxhighlight lang="lean">
   def hello := "Hello, Lean!"
   #eval hello
   </syntaxhighlight>
3. 打开VS Code的终端，运行Lean：
   <syntaxhighlight lang="bash">
   lake init
   lake build
   </syntaxhighlight>

== 验证安装 ==

运行以下命令检查Lean是否安装成功：
<syntaxhighlight lang="bash">
lean --version
</syntaxhighlight>

输出应类似于：
<syntaxhighlight lang="text">
Lean (version 4.0.0)
</syntaxhighlight>

== 实际案例 ==

以下是一个简单的Lean代码示例，展示如何定义一个函数并验证其正确性：
<syntaxhighlight lang="lean">
def add (a b : Nat) : Nat := a + b

#eval add 2 3  -- 输出：5

theorem add_comm (a b : Nat) : add a b = add b a := by
  simp [add, Nat.add_comm]
</syntaxhighlight>

解释：
* <code>def add</code>定义了一个加法函数。
* <code>#eval add 2 3</code>计算并输出结果。
* <code>theorem add_comm</code>证明了加法的交换律。

== 常见问题与解决方案 ==

{| class="wikitable"
|-
! 问题 !! 解决方案
|-
| Lean未正确安装 || 检查系统路径，确保<code>lean</code>命令可用。
|-
| VS Code未识别Lean文件 || 确保安装了Lean 4扩展，并重启VS Code。
|-
| Lake命令未找到 || 运行<code>lake init</code>初始化项目。
|}

== 总结 ==

本节详细介绍了Lean的安装与环境配置方法，涵盖了Windows、macOS和Linux系统，并提供了开发环境配置指南。通过实际案例和常见问题解答，帮助用户快速上手Lean。接下来，可以继续学习Lean的基础语法和定理证明方法。

== 参见 ==
* [[Lean基础语法]]
* [[Lean定理证明入门]]

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean基础]]