Schläfli classification of regular polytopes

schlafli_classification — a formalization challenge from the lean-eval benchmark.

Notes

§42 of Knill's 'Some Fundamental Theorems in Mathematics'. Schläfli's dimension-by-dimension enumeration of the regular convex polytopes: p_3 = 5 (Euclid XIII — the five Platonic solids), p_4 = 6 (Schläfli's six regular 4-polytopes), and p_d = 3 for every d ≥ 5 (regular simplex, hypercube, cross-polytope). Companion to the broader Platonic classification problem, which additionally records p_2 = ∞. Mathlib has convexHull, extremePoints, IsExposed, vectorSpan, AffineIsometryEquiv, Set.encard but no convex-polytope datatype, no face lattice, no regular-polytope concept, and none of the classification counts. The Challenge ships ~1.5 pages of helper defs (ConvexPolytope, dim, IsFace, Flag, isSymmetry, IsRegular, Similar, regularPolytopes, regularSimilar, platonicCount).

Formal statement

/-- **Schläfli classification.** `p_3 = 5 ∧ p_4 = 6 ∧ ∀ d ≥ 5, p_d = 3`. -/
theorem schlafli_classification :
    platonicCount 3 = 5 ∧
      platonicCount 4 = 6 ∧
        ∀ d, 5 ≤ d → platonicCount d = 3 := by
  sorry

Informal solution sketch

p_3 = 5: any regular 3-polytope has Schläfli symbol {p, q} with p, q ≥ 3 and 1/p + 1/q > 1/2 (the spherical-angle-sum constraint at each vertex), giving exactly (3,3), (4,3), (3,4), (5,3), (3,5) — the five Platonic solids. p_4 = 6: any regular 4-polytope {p, q, r} satisfies the analogous spherical inequality, giving (3,3,3), (4,3,3), (3,3,4), (3,4,3), (5,3,3), (3,3,5) — Schläfli's six. p_d ≥ 5 = 3: in dim ≥ 5 the only solutions to the iterated angle constraint are the regular simplex {3, …, 3, 3}, hypercube {4, 3, …, 3}, and cross-polytope {3, …, 3, 4}. Existence of each candidate is by explicit construction (vertex coordinates); uniqueness within Schläfli class is by induction on dimension via vertex figures.

Source

L. Schläfli, Theorie der vielfachen Kontinuität (1852, posthumously published 1901; first proof that p_3 = 5, p_4 = 6, and p_d = 3 for d ≥ 5). Listed as §42 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: schlafli_classification
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.