5 ms·
Rupert's Property
- pavel_lishin 1y agoThey came up with a great name for it.
- bediger4000 1y agoI could not find a Rupert's cube for sale, only thingiverse files to print one. Seems like a missed opportunity, given that you can sell Gombocs at hundreds of dollars each.
- pavel_lishin 1y agoI could have sworn that Matt Parker did a video on this as well, but I couldn't find one.
- jerf 1y agohttps://youtu.be/gPIRLQZnRNk https://youtu.be/gPIRLQZnRNk , 7:20 specifically for cubes. I knew I'd seen it before too so you nerd-sniped me.
- pavel_lishin 1y agoThanks!
- dwrensha 1y agoLast 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/1eb048ae6fa07827fc4e32841ff6ab2fdab56de5/FormalConjectures/Paper/Rupert.lean https://github.com/google-deepmind/formal-conjectures/blob/1... I wonder how feasible it would be to formalize this new proof in Lean.
- yorwba 1y agoThe 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.
- robinhouston 1y agoInteresting. 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 https://youtu.be/jDTPBdxmxKw
- dwrensha 1y ago> 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 https://arxiv.org/abs/2403.17370
- mananaysiempre 1y agoThat sounds like the current proof is too brute-force—too badly understood by humans—for humans to be able to explain it to Lean?
- 1y ago
- karmakaze 1y agoIntuitively 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.
- Strilanc 1y agoOh 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 https://sigbovik.org/2025/proceedings.pdf#page=346
- robinhouston 1y agoI 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.
- clgeoio 1y agoI just read this yesterday, how serendipodus
- decimalenough 1y agoI 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-familys-staggering-real-estate-portfolio https://www.architecturaldigest.com/story/the-murdoch-family...
- nroets 1y agoI was thinking of a different billionaire: https://en.wikipedia.org/wiki/Johann_Rupert https://en.wikipedia.org/wiki/Johann_Rupert
- throw0101c 1y agoAs a Canadian something else came to mind: * https://en.wikipedia.org/wiki/Rupert%27s_Land https://en.wikipedia.org/wiki/Rupert%27s_Land
- robinhouston 1y agoBut this is the same Rupert that we're talking about here!
- evrennetwork 1y ago[dead]
- B1FF_PSUVM 1y ago"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+meme https://www.google.com/search?q=it+goes+into+the+square+hole... ...
- oersted 1y agoHere's the Rupert in question. What a dude! Eminently impressive. https://en.wikipedia.org/wiki/Prince_Rupert_of_the_Rhine https://en.wikipedia.org/wiki/Prince_Rupert_of_the_Rhine
- mci 1y agoHe is also known from prince Rupert's drops. https://en.wikipedia.org/wiki/Prince_Rupert%27s_drop https://en.wikipedia.org/wiki/Prince_Rupert%27s_drop
- armoredkitten 1y agoWhen 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 https://en.wikipedia.org/wiki/Rupert%27s_Land