The septopert is a seven-vertex nopert polyhedron constructed by Murphy (2026). A nopert polyhedron admits no passage with positive clearance of a congruent copy, without turning, through a straight tunnel (Steininger and Yurkevich 2023).
It is the convex hull of the seven points 
, 
, 
, 
, 
, 
,
and 
. It has 15 edges
and 10 triangular faces. Its
symmetry group has Schönflies
symbol 
, with a threefold rotation
axis along 
and three reflection planes. The three edges
meeting at 
are mutually perpendicular (Murphy 2026).
The septopert attains the minimum possible number of vertices of a nopert polyhedron. The accompanying formalization gives a kernel-only Lean proof that every bounded convex polyhedron with nonempty interior and at most six vertices has Rupert's property (Murphy 2026). The minimality concerns the number of vertices, rather than volume or surface area.
The proof that the septopert lacks Rupert's property has a different verification requirement. Its kernel-checked theorem is conditional on the validity of certificate data. Those certificates are checked by compiled Lean code, so this step also trusts the Lean compiler and runtime (Murphy 2026). Its Nieuwland number is 1.
