I'm working on formalizing https://arxiv.org/pdf/2508.18475 https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4 I'm only

I'm working on formalizing https://arxiv.org/pdf/2508.18475 https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4 I'm only on lemma 11 at this point, and up until that point the paper has been fairly easy to formalize (modulo my unfamiliarity with mathlib). The repo is here https://github.com/badly-drawn-wizards/noperthedron https://github.com/badly-drawn-wizards/noperthedron