Mathlib Map

Map · 51

geometry

MSC 51 · Geometry

3,805 declarations (3,344 theorems, 461 definitions) across 76 files. 8 of the 99 famous theorems listed for this area are in Mathlib (8%), 9 in some Lean library. 31 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas5

  • 51M Real and complex geometry 2,279
  • 51A Linear incidence geometry 1,087
  • 51N Analytic and descriptive geometry 229
  • 51K Distance geometry 200
  • 51E Finite geometry and special incidence structures 10

Famous theorems8 of 99

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 91

In Mathlib · 8

From the 100 theorems list7

Open conjectures stated in Lean31

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing15 of 29

From Mathlib's own undergraduate checklist.

Affine and Euclidean Geometry · 15 of 29

  • General definitions › equations of affine subspace
  • General definitions › affine property
  • General definitions › group generated by homotheties and translations
  • General definitions › transformations fixing a basis of directions
  • Euclidean affine spaces › isometries that do and do not preserve orientation
  • Euclidean affine spaces › direct and opposite similarities of the plane
  • Euclidean affine spaces › classification of isometries in two and three dimensions
  • Euclidean affine spaces › angles between planes
  • Euclidean affine spaces › group of isometries stabilizing a subset of the plane or of space
  • Euclidean affine spaces › regular polygons
  • Euclidean affine spaces › metric relations in the triangle
  • Euclidean affine spaces › using complex numbers in plane geometry
  • Application of quadratic forms to study proper conic sections of the affine Euclidean plane › focus
  • Application of quadratic forms to study proper conic sections of the affine Euclidean plane › eccentricity
  • Application of quadratic forms to study proper conic sections of the affine Euclidean plane › quadric surfaces in 3-dimensional Euclidean affine spaces

Files76

Largest first. The code after each file is its assigned subarea.