Rupert.lean
This project is a (work in progress) formalization of the Rupert Problem in the Lean theorem prover.
Roughly speaking, the problem asks: given two congruent copies of a convex polyhedron, can we cut a hole in one copy, such that the other copy fits through the hole?
Known solutions for Platonic, Catalan, and Archimedean solids are visualized in this video:
