编辑“︁Lean在线课程”︁（章节）

== 主要在线课程推荐 ==
以下是当前值得关注的Lean在线课程资源：

=== 1. 官方互动教程 ===
Lean官方提供的交互式学习平台，适合零基础入门：
<syntaxhighlight lang="lean">
-- 示例：基础命题证明
example (P Q : Prop) : P → Q → P ∧ Q :=
begin
  intro hP,
  intro hQ,
  split,
  exact hP,
  exact hQ
end
</syntaxhighlight>
'''输出说明'''：这段代码展示了如何使用Lean的tactics（策略）来构造一个简单命题的证明。

=== 2. 大学公开课 ===
多所顶尖大学提供包含Lean内容的数理逻辑课程：
* 课程结构通常包含：
<mermaid>
graph LR
A[基础逻辑] --> B[Lean语法]
B --> C[命题证明]
C --> D[一阶逻辑]
D --> E[高级类型论]
</mermaid>

=== 3. 专项技能课程 ===
针对特定领域的深入课程，例如：
* 使用Lean进行算法验证
* 数学形式化专题
* 硬件验证应用