Lean verification of the Nopert Stellated Tetrahedron paper's theorem parts (not the computational script parts) - View it on GitHub