This is a collaborative project to write a Lean 4 proof that the Noperthedron does not have the Rupert property.
