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