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 self-contained proof of the main theorem will live in ProofOfMainTheorem.lean. This proof currently depends on the sorry axiom due to performance problems in ComputationalStep.lean.

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.