https://youtu.be/gPIRLQZnRNk , 7:20 specifically for cubes.

I knew I'd seen it before too so you nerd-sniped me.

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.

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

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.