From ff4ae7af0f2d2bf0dfe896262b510f05823d4fce Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 May 2026 17:14:45 +0000 Subject: [PATCH] feat: add Platonic classification eval problem MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §42 of Knill's "Some Fundamental Theorems in Mathematics". The count p_d of regular convex d-polytopes up to similarity is (∞, 5, 6, 3, 3, …): ∞ in dim 2, 5 in dim 3 (Euclid XIII), 6 in dim 4 (Schläfli 1850s), 3 in every dim ≥ 5. Mathlib has the supporting convex-geometry machinery but no convex-polytope datatype, face lattice, regular-polytope concept, or classification counts. The Challenge ships ~1.5 pages of helper defs. Co-Authored-By: Claude Opus 4.7 (1M context) --- LeanEval/Geometry/PlatonicClassification.lean | 117 ++++++++++++++++++ .../problems/platonic_classification.toml | 9 ++ 2 files changed, 126 insertions(+) create mode 100644 LeanEval/Geometry/PlatonicClassification.lean create mode 100644 manifests/problems/platonic_classification.toml diff --git a/LeanEval/Geometry/PlatonicClassification.lean b/LeanEval/Geometry/PlatonicClassification.lean new file mode 100644 index 0000000..4cf1023 --- /dev/null +++ b/LeanEval/Geometry/PlatonicClassification.lean @@ -0,0 +1,117 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace Geometry + +/-! +# Platonic classification + +§42 of Knill's *Some Fundamental Theorems in Mathematics*. The count +`p_d` of regular convex `d`-polytopes (Platonic polytopes) up to +similarity is `p_2 = ∞` (regular polygons), `p_3 = 5` (Euclid XIII — +tetrahedron, cube, octahedron, dodecahedron, icosahedron), `p_4 = 6` +(Schläfli 1850s — 5-cell, 8-cell, 16-cell, 24-cell, 120-cell, 600-cell), +and `p_d = 3` for every `d ≥ 5` (regular simplex, hypercube, +cross-polytope). + +mathlib has `convexHull`, `extremePoints`, `IsExposed`, `vectorSpan`, +`AffineIsometryEquiv`, and `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 definitions +(`ConvexPolytope`, `dim`, `IsFace`, `Flag`, `isSymmetry`, `IsRegular`, +`Similar`, `regularPolytopes`, `regularSimilar`, `platonicCount`) on top +of mathlib. +-/ + +open scoped Topology + +/-- The Euclidean model space `ℝⁿ`. -/ +abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin n) + +/-- A **convex polytope** in `ℝⁿ`: the convex hull of a finite nonempty set +whose listed vertices are exactly the extreme points of the hull. -/ +structure ConvexPolytope (n : ℕ) where + vertices : Finset (E n) + vertices_nonempty : vertices.Nonempty + vertices_eq_extremePoints : + (vertices : Set (E n)) = + Set.extremePoints ℝ (convexHull ℝ ((vertices : Set (E n)))) + +namespace ConvexPolytope + +/-- The underlying convex set of the polytope. -/ +def toSet {n : ℕ} (P : ConvexPolytope n) : Set (E n) := + convexHull ℝ ((P.vertices : Set (E n))) + +/-- The affine dimension of `P`. -/ +noncomputable def dim {n : ℕ} (P : ConvexPolytope n) : ℕ := + Module.finrank ℝ (vectorSpan ℝ P.toSet) + +/-- `P` is **full-dimensional** if `dim P = n`. -/ +def IsFullDim {n : ℕ} (P : ConvexPolytope n) : Prop := P.dim = n + +/-- A **face** of `P` is a nonempty exposed subset. -/ +def IsFace {n : ℕ} (P : ConvexPolytope n) (F : Set (E n)) : Prop := + IsExposed ℝ P.toSet F ∧ F.Nonempty + +/-- The affine dimension of a subset of `ℝⁿ`. -/ +noncomputable def faceDim {n : ℕ} (F : Set (E n)) : ℕ := + Module.finrank ℝ (vectorSpan ℝ F) + +/-- A **flag** of a full-dimensional `n`-polytope `P`: a strictly +increasing chain `F_0 ⊂ F_1 ⊂ ⋯ ⊂ F_{n−1}` of faces with `faceDim F_k = k`. -/ +structure Flag {n : ℕ} (P : ConvexPolytope n) where + face : Fin n → Set (E n) + isFace : ∀ k, P.IsFace (face k) + dim_eq : ∀ k : Fin n, faceDim (face k) = k.val + strict_mono : ∀ i j : Fin n, i < j → face i ⊂ face j + +/-- Affine isometries of `ℝⁿ` — the rigid motions. -/ +abbrev Isom (n : ℕ) := E n ≃ᵃⁱ[ℝ] E n + +/-- `φ` is a **symmetry** of `P` if it maps `P` onto itself. -/ +def isSymmetry {n : ℕ} (P : ConvexPolytope n) (φ : Isom n) : Prop := + ((φ : E n → E n)) '' P.toSet = P.toSet + +/-- `P` is **regular** (Platonic) if it is full-dimensional and its +symmetry group acts transitively on its flags. -/ +def IsRegular {n : ℕ} (P : ConvexPolytope n) : Prop := + P.IsFullDim ∧ + ∀ F G : P.Flag, ∃ φ : Isom n, + P.isSymmetry φ ∧ + ∀ k : Fin n, ((φ : E n → E n)) '' F.face k = G.face k + +/-- Two polytopes are **similar** when related by a positive scaling and an +affine isometry. -/ +def Similar {n : ℕ} (P Q : ConvexPolytope n) : Prop := + ∃ a : ℝ, 0 < a ∧ ∃ φ : Isom n, + Q.toSet = (fun x : E n => a • x) '' ((φ : E n → E n) '' P.toSet) + +end ConvexPolytope + +/-- The set of regular (Platonic) polytopes in dimension `d`. -/ +def regularPolytopes (d : ℕ) : Set (ConvexPolytope d) := + {P | P.IsRegular} + +/-- The similarity relation on regular polytopes in dimension `d`. -/ +def regularSimilar (d : ℕ) (P Q : regularPolytopes d) : Prop := + ConvexPolytope.Similar (P : ConvexPolytope d) (Q : ConvexPolytope d) + +/-- `p_d` — count of Platonic polytopes in dimension `d` up to similarity, +in `ℕ∞ = ℕ ∪ {⊤}` so `⊤` records "infinitely many". -/ +noncomputable def platonicCount (d : ℕ) : ℕ∞ := + Set.encard {S : Set (regularPolytopes d) | + ∃ P, S = {Q : regularPolytopes d | regularSimilar d P Q}} + +/-- **Platonic classification.** `p = (p_2, p_3, p_4, p_5, …) = (∞, 5, 6, 3, 3, 3, …)`. -/ +@[eval_problem] +theorem platonic_classification : + platonicCount 2 = ⊤ ∧ + platonicCount 3 = 5 ∧ + platonicCount 4 = 6 ∧ + ∀ d, 5 ≤ d → platonicCount d = 3 := by + sorry + +end Geometry +end LeanEval diff --git a/manifests/problems/platonic_classification.toml b/manifests/problems/platonic_classification.toml new file mode 100644 index 0000000..e2f6d63 --- /dev/null +++ b/manifests/problems/platonic_classification.toml @@ -0,0 +1,9 @@ +id = "platonic_classification" +title = "Platonic classification" +test = false +module = "LeanEval.Geometry.PlatonicClassification" +holes = ["platonic_classification"] +submitter = "Kim Morrison" +notes = "§42 of Knill's 'Some Fundamental Theorems in Mathematics'. The count p_d of regular convex d-polytopes (Platonic polytopes) up to similarity is p_2 = ∞ (regular polygons), p_3 = 5 (Euclid XIII), p_4 = 6 (Schläfli 1850s), and p_d = 3 for d ≥ 5. 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)." +source = "Euclid, Elements, Book XIII (~300 BC, p_3 = 5); L. Schläfli, Theorie der vielfachen Kontinuität (1852, posthumous publication; p_4 = 6, 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)." +informal_solution = "p_2 = ⊤: for each n ≥ 3 the regular n-gon (vertices = n-th roots of unity) is regular and any two non-congruent regular polygons are non-similar; the construction gives infinitely many similarity classes. 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."