The convex uniform 5-polytopes: a computer-assisted classification

We prove completeness of the convex uniform 5-polytope list, conditional on the cited lower-dimensional classifications, the written reductions and the certificate checkers. Its members are Wythoff's constructions of types $A_5$, $B_5$, $D_5$, prisms over uniform 4-polytopes, and products of regular polygons with uniform polyhedra. Conway and Guy announced the four-dimensional classification; Möller gave a complete computer-assisted proof. We extend these neighborhood and radius methods to dimension five. Coxeter's and Johnson's constructions supply the known families. Unbounded polygon sizes require products, forced by neighbor distances and prism cells. Lean checks a conditional implication from explicit premises.

Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.