I 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.
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
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.
12 comments
[ 3.3 ms ] story [ 37.5 ms ] threadhttps://github.com/google-deepmind/formal-conjectures/blob/1...
I wonder how feasible it would be to formalize this new proof in Lean.
David Renshaw recently gave a formal proof in Lean that the triakis tetrahedron does have Rupert's property: https://youtu.be/jDTPBdxmxKw
I would hope there are others with more faces that don't have the property and this could have the fewest faces.
https://www.architecturaldigest.com/story/the-murdoch-family...
Audience pretending not to think of https://www.google.com/search?q=it+goes+into+the+square+hole... ...
https://en.wikipedia.org/wiki/Prince_Rupert_of_the_Rhine