Comment by dwrensha

Last month, before this result came out, the question "Is Every Convex Polyhedron Rupert?" was added as a formal Lean statement to Google's Formal Conjectures repository:

https://github.com/google-deepmind/formal-conjectures/blob/1...

I wonder how feasible it would be to formalize this new proof in Lean.