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".

noperthedron

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

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

Construction of a valid solution table requires a large case analysis. We provide three different versions:

A kernel-only proof KernelCaseAnalysis/ProofOfMainTheorem.lean that depends only on the standard 3 axioms [propext, Classical.choice, Quot.sound]. This proof takes ~2.5 hours to check on a 16-core machine.
A native_decide proof NativeCaseAnalysis/ProofOfMainTheorem.lean that takes ~3 minutes on a 16-core machine.
A native executable constructValidTable that takes ~1 minute to run on a 16-core machine.

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

lake exe cache get
lake build

To check the solution table, first make sure that you have git-lfs. Then unzip the table:

unzip solution_tree_v6.zip

To run the expensive kernel check (~50 core hours):

lake build KernelCaseAnalysis

To run the less expensive native_decide check (~1 core hour):

lake build NativeCaseAnalysis

To run the even less expensive native executable check (~0.25 core hour) :

lake exe constructValidTable solution_tree_v6.csv

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