>One of the perennial questions about proof automation has been the utility of proofs that cannot be understood by humans.

I'm skeptical of an in-principle impossibility of understanding complex proofs. I think computers likely will have, or already do have, a capability for explaining proofs piecemeal, with explanations that bridge from the proof itself to familiar intuitions.

Needing to understanding by increasingly sophisticated bridge explanations may be us getting further removed from immediate understanding but I don't think it crosses a magical threshold or anything that fundamentally calls into question how operational/useful the proofs are.