I would say this is why formal proofs (and things like the Lean 4 libs) are so important, so that you can deconstruct the tower provably back into pieces you can understand. It shouldn't be possible to construct a formal proof you cannot destructure like this.

As a (crude) analogy, it's a bit like how you can prove the healthiness of a git tree because it's a graph of content hashes and the tree graph pointers are part of the hash. Imagine this but with a tree of knowledge.