Noperts: Reproducible proofs of non-Rupert polyhedra

A collection of formal, reproducible verifications that several convex polyhedra do not have Rupert's property (cannot pass a congruent copy of themselves through themselves). It includes Lean proofs that the snub dodecahedron, pentagonal hexecontahedron, and deltoidal hexecontahedron are Nopert, a repaired candidate labeled #231, and a newly discovered seven‑vertex Nopert called the Septopert. Together with earlier verifications and claimed results for other solids, this completes a classification of the Platonic, Archimedean and Catalan families with respect to Ruperty, and it proves kernel‑only in Lean that every convex polyhedron with six or fewer vertices is Rupert, making the Septopert minimal by vertex count.

The verifications combine kernel Lean theorems with large external certificates generated by C++ search code: the Lean statement is a small, trusted kernel proof of the implication “if the certificate validator accepts, then the solid is Nopert,” while the certificates themselves (many gigabytes; the Septopert certificate is ~7 GB) are produced and checked by programs. Reproduction requires rebuilding those certificates with provided scripts; verification of the Septopert took about four hours on a 64‑core machine. The Septopert geometry, symmetry (C3v), vertex coordinates (fit 32‑bit floats) and an STL for printing are included. Work builds on prior formalizations (Steininger & Yurkevich; Jason Reed et al.), used AI-assisted search and repair during development, and is released under Apache‑2.0 for Lean code and GPLv3 for most C++.