Rupert.lean
This project is a 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?
The proof for the triakis tetrahedron is explained in this video:
Known solutions for Platonic, Catalan, and Archimedean solids are visualized in this video:
