编辑“︁Lean mathlib介绍”︁（章节）

== 实际应用案例 ==

=== 形式化微积分 ===

mathlib 包含完整的微积分库，例如下面形式化的导数定义：

<math>
\frac{d}{dx}f(x) = \lim_{h \to 0}\frac{f(x+h)-f(x)}{h}
</math>

对应的 Lean 形式化为：

<syntaxhighlight lang="lean">
import Mathlib.Analysis.Calculus.Deriv.Basic

def formal_derivative {𝕜 : Type} [NontriviallyNormedField 𝕜]
  {E : Type} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  (f : 𝕜 → E) (x : 𝕜) := deriv f x
</syntaxhighlight>

=== 机器学习应用 ===

mathlib 的线性代数部分可用于机器学习算法的形式化验证：

<syntaxhighlight lang="lean">
import Mathlib.LinearAlgebra.Matrix

-- 定义简单的神经网络层
def dense_layer (W : Matrix ℝ m n) (b : Vector ℝ n) (x : Vector ℝ m) :=
  W * x + b  -- 矩阵乘法和向量加法
</syntaxhighlight>