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

A convex polytope is uniform if its symmetries act transitively on its vertices and its facets are uniform, down to regular polygons. We give a computer-assisted completeness proof for the known convex uniform 5-polytopes: Wythoff constructions of types A₅, B₅ and D₅, prisms over convex uniform 4-polytopes, and products of regular polygons with convex uniform polyhedra. The theorem holds conditional on the cited 3-D and Conway–Guy–Möller 4-D classifications, the correctness of the written reductions in the paper, and the correctness of the certificate checkers. For faces with at most 16 sides, enumeration covers all possible vertex neighborhoods, identifies 628 known polytopes and rules out one additional candidate; a face with at least 17 sides forces a product. This extends Möller's method to dimension five and produces no new examples.