Lean几何库

Lean几何库

简介

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

核心概念

基本对象定义

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 }

公理与定理

库中实现了欧几里得公理体系，例如“两点确定一条直线”可形式化为：

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

实际案例

验证三角形全等

以下代码演示如何证明“边角边”（SAS）全等定理：

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

可视化辅助

使用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

高级应用

与拓扑库集成

几何对象可转换为拓扑空间，例如证明圆同胚于实射影直线：

import Mathlib.Topology.Algebra.ProjectiveSpace

example : EuclideanGeometry.Circle ℝ ≃ₜ ProjectiveSpace ℝ 1 :=
  Circle.equivRealProjectiveLine

复杂定理证明

形式化“九点圆定理”的核心步骤：

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

数学公式支持

库中涉及的关键公式如圆的方程： $(x-h{)}^2+(y-k{)}^2=r^2$

学习建议

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

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