Classification of Five-Dimensional Reflexive Polytopes Arising from Single Weight Systems

We present a computational pipeline, along with two layers of formal verification, for the exhaustive GL(5,Z)-classification within the one-equation weight system sector in dimension five: the Newton polytopes arising from the complete Schöller–Skarke list of length-six weight systems. The combined weight systems and the subsequent reflexive-subpolytope search are not part of the present computation, so the catalogues reported here are complete for the single weight system sector and are explicitly not a classification of all five-dimensional reflexive polytopes. Starting from the Schöller–Skarke dataset of approximately 185 billion reflexive and 137 billion IP weight systems, we compute the GL(5,Z) normal form of each associated polytope, hash the resulting canonical matrix, and deduplicate across the full dataset using a two-phase sort-merge algorithm. The pipeline processes the 4.7 TB input dataset across distributed compute nodes, producing two single weight system catalogues: 2,377,115,412 unique reflexive polytopes and 11,469,405,637 unique IP polytopes (non-reflexive), each with frequency counts and associated geometric invariants. Correctness is established at two levels. At the theoretical level, we report a Lean 4 formalization of the Kreuzer–Skarke classification chain whose main result is the completeness of the single weight system enumeration algorithm within this stated scope. At the level of the implementation, bounded model checking (CBMC) and abstract interpretation (Frama-C) establish the correctness of the C/C++ models and routines.