ElementarGeometrie

A Lean 4 formalization of the foundations of elementary geometry — incidence geometries, affine incidence planes, and projective spaces — built on top of Mathlib.

The development follows the lecture notes Elementargeometrie by Wolfgang Soergel (Universität Freiburg). Terminology and documentation are in English.

Status. The full architecture compiles cleanly against Mathlib. The structural backbone is fully proved; a handful of deep classical theorems (Hilbert-style coordinatization and characterization results) are stated and left as explicit goals.

---

What is formalized

The theory is built in three layers, each resting on the previous one.

1 · Incidence geometry

An incidence geometry is a set X with a system of lines lines : Set (Set X) such that every line has at least two points and any two distinct points lie on exactly one line.

• Incidence/Basic.lean — the structure, the join line x y, collinearity, concurrence, triangles, and collineations (isomorphisms of incidence geometries).
• Incidence/Betweenness.lean — betweenness relations (Zwischenrelation) with compatible orderings and Pasch's axiom; segments and rays.
• Incidence/Congruence.lean — congruence groups, the supremum property, near-Euclidean geometries, and the parallel axiom.

2 · Affine incidence planes

An affine incidence plane adds the parallel axiom (a unique parallel through every off-line point) and the existence of a triangle.

• Affine/Plane.lean — the structure and the relation ∥ ("equal or parallel"), proved to be an equivalence on lines.
• Affine/Desargues.lean — the Desargues property and its degenerate variant.
• Affine/Pappus.lean — the Pappus property and Pappus planes.

3 · Projective spaces

• Projective/Space.lean — the projectivization ℙ K V of a vector space, made into an incidence geometry.
• Projective/Completion.lean — the projective completion E ⊕ ℙ K V of an affine space, with its points at infinity.
• Projective/Duality.lean — incidence structures, the dual of an incidence structure, and the point–line duality theorem for a three-dimensional vector space.

Standard models

• Examples.lean — the standard affine plane K² over a division ring, and the real plane ℝ² as the case K = ℝ.

---

Proof status

Result	File	State
ℙ K V is an incidence geometry	Projective/Space.lean	✅
K² is an affine incidence plane	Examples.lean	✅
∥ is an equivalence relation on lines	Affine/Plane.lean	✅
Point–line duality ℙ(V*) ≅ ℙ(V)-dual	Projective/Duality.lean	✅
Projective completion is an incidence geometry	Projective/Completion.lean	✅
Pappus ⇒ Desargues	Affine/Pappus.lean	🚧
Degenerate Desargues	Affine/Desargues.lean	🚧
Coordinatization: Desargues ⟺ K²	Examples.lean	🚧
ℝ² is a Pappus plane	Examples.lean	🚧
Characterization of the Euclidean plane	Incidence/Congruence.lean	🚧

✅ = fully proved  ·  🚧 = stated, proof in progress (sorry).

The 🚧 entries are genuine classical theorems (Hilbert-style coordinatization and characterization arguments) recorded as explicit goals for future work.

---

Building

The project pins its toolchain in lean-toolchain (leanprover/lean4:v4.32.0-rc1) and its Mathlib revision in lakefile.toml. With elan installed:

# fetch the prebuilt Mathlib cache (recommended — avoids recompiling Mathlib)
lake exe cache get

# build the whole library
lake build

To check a single module, for example:

lake build ElementarGeometrie.Projective.Duality

---

Conventions

• One carrier type X, with lines modeled faithfully as Set (Set X), so that a line is a subset and "lies on" is literal set membership.
• English terminology throughout, with the original German terms recorded in doc-strings (e.g. Zwischenrelation, fasteuklidische Geometrie).
• Every top-level declaration carries a doc-string, and the build runs Mathlib's standard linter set (weak.linter.mathlibStandardSet).

---

Source

The mathematical content follows W. Soergel, Elementargeometrie (Universität Freiburg); the LaTeX source used as a reference lives under Soergel/.

License

Released under the Apache 2.0 license — see LICENSE.