编辑“︁Lean公理系统”︁（章节）

== 代码示例 ==
以下展示Lean中公理声明的实际语法：

<syntaxhighlight lang="lean">
-- 函数外延性公理
axiom funext {α β : Type} {f g : α → β} 
  (h : ∀ x, f x = g x) : f = g

-- 自然数的Peano公理
inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat
</syntaxhighlight>

'''输入验证'''：尝试证明基本命题：
<syntaxhighlight lang="lean">
example (f : Nat → Nat) : f ∘ id = f := 
by 
  apply funext  -- 应用函数外延性
  intro x       -- 引入任意x
  rfl           -- 根据定义得证
</syntaxhighlight>
'''输出结果'''：Lean成功验证<code>f ∘ id = f</code>的证明。