Rupert's Property

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?

But this is the same Rupert that we're talking about here!