编辑“︁Lean几何库”︁（章节）

= Lean几何库 =

== 简介 ==  
'''Lean几何库'''是[[Lean定理证明器]]中用于形式化几何概念的数学库，基于[[欧几里得几何]]公理体系构建。它为使用者提供了定义点、线、圆等基本几何对象的能力，并允许通过交互式证明验证几何定理。该库是[[Lean数学库]]（Mathlib）的一部分，与代数、拓扑等模块深度集成，适合从初学者到研究者的多层次需求。

== 核心概念 ==  

=== 基本对象定义 ===  
Lean几何库通过类型论定义几何对象。以下示例展示点、直线和圆的构造：  

<syntaxhighlight lang="lean">
import Mathlib.Geometry.Euclidean.Basic

-- 定义点、直线和圆
def pointA : EuclideanSpace ℝ 2 := ![1.0, 0.0]
def lineAB : AffineSubspace ℝ (EuclideanSpace ℝ 2) := 
  AffineSubspace.mk' pointA (![2.0, 1.0])  -- 通过点和方向向量构造直线
def circle : EuclideanGeometry.Circle ℝ := 
  { center := ![0.0, 0.0], radius := 3.0 }
</syntaxhighlight>

=== 公理与定理 ===  
库中实现了欧几里得公理体系，例如“两点确定一条直线”可形式化为：  
<syntaxhighlight lang="lean">
theorem line_unique (p q : EuclideanSpace ℝ 2) (h : p ≠ q) :
  ∃! (l : AffineSubspace ℝ (EuclideanSpace ℝ 2)), p ∈ l ∧ q ∈ l := by
  apply EuclideanGeometry.line_through_unique
  exact h
</syntaxhighlight>

== 实际案例 ==  

=== 验证三角形全等 ===  
以下代码演示如何证明“边角边”（SAS）全等定理：  
<syntaxhighlight lang="lean">
import Mathlib.Geometry.Euclidean.Triangle

-- 定义两个三角形
def ΔABC : Triangle ℝ := ⟨![0,0], ![1,0], ![0,1]⟩
def ΔDEF : Triangle ℝ := ⟨![2,2], ![3,2], ![2,3]⟩

-- SAS条件：AB=DE, ∠BAC=∠EDF, AC=DF
example (hAB : dist ΔABC.point₁ ΔABC.point₂ = dist ΔDEF.point₁ ΔDEF.point₂)
        (hAC : dist ΔABC.point₁ ΔABC.point₃ = dist ΔDEF.point₁ ΔDEF.point₃)
        (hAngle : ∠ ΔABC.point₁ ΔABC.point₂ ΔABC.point₃ = ∠ ΔDEF.point₁ ΔDEF.point₂ ΔDEF.point₃) :
        ΔABC ≅ ΔDEF := by
  apply Triangle.congruent_of_SAS
  repeat' assumption
</syntaxhighlight>

=== 可视化辅助 ===  
使用Mermaid绘制几何关系图：  
<mermaid>
graph TD
  A[点A] -->|距离=3| B[点B]
  A --> C[点C]
  B --> C
  style A fill:#f9f,stroke:#333
  style B fill:#bbf,stroke:#333
</mermaid>

== 高级应用 ==  

=== 与拓扑库集成 ===  
几何对象可转换为拓扑空间，例如证明圆同胚于实射影直线：  
<syntaxhighlight lang="lean">
import Mathlib.Topology.Algebra.ProjectiveSpace

example : EuclideanGeometry.Circle ℝ ≃ₜ ProjectiveSpace ℝ 1 :=
  Circle.equivRealProjectiveLine
</syntaxhighlight>

=== 复杂定理证明 ===  
形式化“九点圆定理”的核心步骤：  
<syntaxhighlight lang="lean">
theorem nine_point_circle (Δ : Triangle ℝ) :
  let midpoint := fun (a b : ℝ²) => (a + b) / 2;
  ∃ (c : EuclideanGeometry.Circle ℝ),
    c.PassesThrough (midpoint Δ.point₁ Δ.point₂) ∧
    c.PassesThrough (midpoint Δ.point₂ Δ.point₃) ∧
    -- 其余7个点条件省略
    True := by
  apply exists_nine_point_circle
</syntaxhighlight>

== 数学公式支持 ==  
库中涉及的关键公式如圆的方程：  
<math>
(x - h)^2 + (y - k)^2 = r^2
</math>

== 学习建议 ==  
* 初学者应从`Euclidean.Basic`模块入手，熟悉向量构造。
* 中级用户可尝试复现《几何原本》中的经典命题。
* 研究者可探索与微分几何的交叉领域（如曲率形式化）。

该库持续扩展，最新功能建议查阅Mathlib的更新日志。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean与数学库]]