Noperthedron

This project formalizes the main result of "A convex polyhedron without Rupert's property" by Jakob Steininger & Sergey Yurkevich (cited as [SY25] herein).

We prove, using the Lean 4 theorem prover, that the Noperthedron does not "fit through itself".

See the dependency graph for an overview of the project's structure.

The proof involves constructing a large tree object and verifying that it has certain properties. The original authors performed their version of this computation using Sagemath. We perform the computation in a natively-compiled Lean program that emits a value of a carefully crafted type called ValidTable.

Project Structure

The definition of the main theorem proposition lives in MainTheorem.lean.

The proof of the main theorem, given existence of a valid solution table, lives in ProofOfMainTheoremWithHole.lean.

The program to construct a valid solution table is constructValidTable.lean.

The complete proof of the main theorem lives in ProofOfMainTheorem.lean. Its most expensive step, in ComputationalStep.lean, is commented out and replaced by a sorry so that every CI run does not take days to complete.

Getting Started

Install Lean, clone this project, then build it with:

lake exe cache get
lake build

To build the blueprint, install leanblueprint with something like

pip install leanblueprint

Then you can build all HTML and PDF content and check correspondence of blueprint decls (i.e. uses of \lean) with actual lean identifiers by doing

leanblueprint all

To run a server hosting the html, run

leanblueprint serve

License Information

Portions of this project use Apache License 2.0–licensed code from https://github.com/badly-drawn-wizards/noperthedron ©2025 Reuben Steenekamp See LICENSE for details.