I believe that the name ‘Noperthedron’ for this new polyhedron that has been proven not to be Rupert was given in homage to tom7’s coinage ‘Nopert’ in that SIGBOVIK paper.
Last month, before this result came out, the question "Is Every Convex Polyhedron Rupert?" was added as a formal Lean statement to Google's Formal Conjectures repository:
Interesting. My guess is that it's not prohibitively hard, and that someone will probably do it. (There may be a technical difficulty I don't know about, though.)
David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property: https://youtu.be/jDTPBdxmxKw
> David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property
That's me!
This result appears to be significantly harder to formalize.
Steininger and Yurkevich's proof certificate is a 2.5GB tree that partitions the state space into 18 million cells and takes 30 hours to validate in SageMath.
Formalizing the various helper lemmas in the paper does seem achievable to me, but I suspect that applying them to all of the millions of cells as part of a single Lean theorem could present some significant engineering difficulties. I think it'd be a fun challenge!
If that turns out to be infeasible, an alternate approach might be: we could write a Lean proof that the 2.5GB tree faithfully encodes the original problem, while still delegating the validation of that tree to an external SageMath process. Such a formalization would at least increase our confidence that there are no math errors in the setup. A similar approach was taken recently by Bernardo Subercaseaux et al in their recent paper where they formally verified a SAT-solver encoding for the "empty hexagon number": https://arxiv.org/abs/2403.17370
Lean does feasibly let you shard out verification work; i.e., you can take a huge proof tree, chop it into an assortment of independently-proven branches (trivial if it's a true tree), let those branches be verified in parallel by a simple cluster, inject the feedback information from the cluster tasks ("this theorem here (the open goals/interactive state at the point this branch was cut out of the full tree) is true; no need for you to actually be aware that it's proven with specifically this proof here (the branch of the tree)") into the main kernel's verification cache (or just declare those intermediate theorems as true), and write a "apply this_theorem_we_cut_out_here" in place of the cut-out branch when writing up the main tree.
Good thing that, as long as you verify the entire result and make sure your verifier orchestration doesn't have bugs of a "cheating" nature, you can let AI run pretty wild on transforming/translating/chopping a Lean proof tree, because the verifier is already presumed to be an oracle with no false positives.
E.g. here it could potentially help translating SageMath representations to Lean4 representations, with the only downside that a failed verification in Lean could be due to merely erroneous AI-assisted translation.
Overall, I'd think given the nature of proving that a polyhedron doesn't have Rupert's property, there should be fairly straight-forward (if not actually trivial) ways of sharding the proof.
The paper seems to talk of a 5-dimensional search space; in more general I'd think it's 8 dimensions to account for the translation through the proposed hole (this is still assuming you want to not rotate the polyhedra as you're passing one through the other):
"attack direction (angle of the penetrated)" from any direction (3D; unit quaternion),
while the penetrator is facing any direction (3D; unit quaternion),
shifted sideways any amount normal to the direction of translation (2D; simple 2D point),
valid at any translation/penetration depth (1D; simple distance/real),
while cancelling one dimension worth of freedom because only mutual twist along the direction translation matters (not absolute twist).
There's some mirror/flip symmetries that each take a factor of 2 out, but that's insignificant as long as we keep the dimensions of our geometry fixed at 3.
Now having thought about it a bit more to write this, I think it'd be mostly (automatable brute-force type) mechanical once you translate the coarse proof structure and theorem definitions, because you're "just" sweeping 5 (or 8) degrees of freedom while partitioning the search space whenever your property definition hits a branch.
A benefit of that being a possibly trivially parallel/flat certificate that's basically composed of 2 parts:
(1) a list of intervals in the 5/8 dimensional search space that together cover the entire search space,
and (2) for each listed interval, a branch-free verifiable statement (certificate) that the property definition applies in a definitionally uniform manner across said interval.
The most annoying bit might be that they use different, though equivalent, definitions of the property, so you would also need to formalize the proof of the equivalence of definitions.
Intuitively not surprising as the property doesn't hold for a sphere which can be approximated. But there's a world of difference between intuition and proof, especially on the edge.
I would hope there are others with more faces that don't have the property and this could have the fewest faces.
When I saw the title "Rupert's Property", I immediately thought of Rupert's Land which used to exist in Canada[0] (a large area around Hudson Bay, essentially). And as it turns out, it's the same guy! So apparently Canada also can be said to have Rupert's Property ;)
Oh damn, in this year's sigbovik, Tom7 was trying to find out if shapes were Rupert or not: https://sigbovik.org/2025/proceedings.pdf#page=346
I just read this yesterday, how serendipodus
I believe that the name ‘Noperthedron’ for this new polyhedron that has been proven not to be Rupert was given in homage to tom7’s coinage ‘Nopert’ in that SIGBOVIK paper.
Last month, before this result came out, the question "Is Every Convex Polyhedron Rupert?" was added as a formal Lean statement to Google's Formal Conjectures repository:
https://github.com/google-deepmind/formal-conjectures/blob/1...
I wonder how feasible it would be to formalize this new proof in Lean.
Interesting. My guess is that it's not prohibitively hard, and that someone will probably do it. (There may be a technical difficulty I don't know about, though.)
David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property: https://youtu.be/jDTPBdxmxKw
> David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property
That's me!
This result appears to be significantly harder to formalize.
Steininger and Yurkevich's proof certificate is a 2.5GB tree that partitions the state space into 18 million cells and takes 30 hours to validate in SageMath.
Formalizing the various helper lemmas in the paper does seem achievable to me, but I suspect that applying them to all of the millions of cells as part of a single Lean theorem could present some significant engineering difficulties. I think it'd be a fun challenge!
If that turns out to be infeasible, an alternate approach might be: we could write a Lean proof that the 2.5GB tree faithfully encodes the original problem, while still delegating the validation of that tree to an external SageMath process. Such a formalization would at least increase our confidence that there are no math errors in the setup. A similar approach was taken recently by Bernardo Subercaseaux et al in their recent paper where they formally verified a SAT-solver encoding for the "empty hexagon number": https://arxiv.org/abs/2403.17370
Lean does feasibly let you shard out verification work; i.e., you can take a huge proof tree, chop it into an assortment of independently-proven branches (trivial if it's a true tree), let those branches be verified in parallel by a simple cluster, inject the feedback information from the cluster tasks ("this theorem here (the open goals/interactive state at the point this branch was cut out of the full tree) is true; no need for you to actually be aware that it's proven with specifically this proof here (the branch of the tree)") into the main kernel's verification cache (or just declare those intermediate theorems as true), and write a "apply this_theorem_we_cut_out_here" in place of the cut-out branch when writing up the main tree.
Good thing that, as long as you verify the entire result and make sure your verifier orchestration doesn't have bugs of a "cheating" nature, you can let AI run pretty wild on transforming/translating/chopping a Lean proof tree, because the verifier is already presumed to be an oracle with no false positives.
E.g. here it could potentially help translating SageMath representations to Lean4 representations, with the only downside that a failed verification in Lean could be due to merely erroneous AI-assisted translation.
Overall, I'd think given the nature of proving that a polyhedron doesn't have Rupert's property, there should be fairly straight-forward (if not actually trivial) ways of sharding the proof. The paper seems to talk of a 5-dimensional search space; in more general I'd think it's 8 dimensions to account for the translation through the proposed hole (this is still assuming you want to not rotate the polyhedra as you're passing one through the other):
"attack direction (angle of the penetrated)" from any direction (3D; unit quaternion), while the penetrator is facing any direction (3D; unit quaternion), shifted sideways any amount normal to the direction of translation (2D; simple 2D point), valid at any translation/penetration depth (1D; simple distance/real), while cancelling one dimension worth of freedom because only mutual twist along the direction translation matters (not absolute twist).
There's some mirror/flip symmetries that each take a factor of 2 out, but that's insignificant as long as we keep the dimensions of our geometry fixed at 3.
Now having thought about it a bit more to write this, I think it'd be mostly (automatable brute-force type) mechanical once you translate the coarse proof structure and theorem definitions, because you're "just" sweeping 5 (or 8) degrees of freedom while partitioning the search space whenever your property definition hits a branch. A benefit of that being a possibly trivially parallel/flat certificate that's basically composed of 2 parts: (1) a list of intervals in the 5/8 dimensional search space that together cover the entire search space, and (2) for each listed interval, a branch-free verifiable statement (certificate) that the property definition applies in a definitionally uniform manner across said interval.
That sounds like the current proof is too brute-force—too badly understood by humans—for humans to be able to explain it to Lean?
The most annoying bit might be that they use different, though equivalent, definitions of the property, so you would also need to formalize the proof of the equivalence of definitions.
Intuitively not surprising as the property doesn't hold for a sphere which can be approximated. But there's a world of difference between intuition and proof, especially on the edge.
I would hope there are others with more faces that don't have the property and this could have the fewest faces.
"You can cut a hole in a cube that’s big enough to slide an identical cube through that hole! Think about that for a minute—it’s kind of weird."
Audience pretending not to think of https://www.google.com/search?q=it+goes+into+the+square+hole... ...
Here's the Rupert in question. What a dude! Eminently impressive.
https://en.wikipedia.org/wiki/Prince_Rupert_of_the_Rhine
When I saw the title "Rupert's Property", I immediately thought of Rupert's Land which used to exist in Canada[0] (a large area around Hudson Bay, essentially). And as it turns out, it's the same guy! So apparently Canada also can be said to have Rupert's Property ;)
[0] https://en.wikipedia.org/wiki/Rupert%27s_Land
He is also known from prince Rupert's drops.
https://en.wikipedia.org/wiki/Prince_Rupert%27s_drop
I was expecting a long listing of real estate owned by Rupert Murdoch. Fortunately somebody else already wrote that one too:
https://www.architecturaldigest.com/story/the-murdoch-family...
I was thinking of a different billionaire:
https://en.wikipedia.org/wiki/Johann_Rupert
As a Canadian something else came to mind:
* https://en.wikipedia.org/wiki/Rupert%27s_Land
But this is the same Rupert that we're talking about here!
I could have sworn that Matt Parker did a video on this as well, but I couldn't find one.
https://youtu.be/gPIRLQZnRNk , 7:20 specifically for cubes.
I knew I'd seen it before too so you nerd-sniped me.
Thanks!
[dead]