Mathlib Map

Map · 52

convex and discrete geometry

MSC 52 · Convex and discrete geometry

2,015 declarations (1,792 theorems, 223 definitions) across 60 files. 5 of the 15 famous theorems listed for this area are in Mathlib (33%). 45 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.

Subareas3

  • 52A General convexity 1,916
  • 52C Discrete geometry 50
  • 52B Polytopes and polyhedra 49

Famous theorems5 of 15

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

Not yet in Mathlib · 10

In Mathlib · 5

Open conjectures stated in Lean45

Statements without proofs, collected by the Formal Conjectures project.

Structures defined here2

Typeclasses defined in this area's files, most assumed first.

Files60

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