> gulf between ... novel proofs and ... understanding

Machine proofs are useful machine understanding. You don't read the proofs, that's holding it wrong. You point another agent at the proof and prompt "use these ideas to prove this lemma that's useful to me". And it works, agents are faster given access to the proofs than without.