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