Comment Comment by reuben364 I'm working on formalizing https://arxiv.org/pdf/2508.18475 (A convex polyhedron without Rupert's property) in Lean4I'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 parent reuben364 11 months ago
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