I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded. But for OP, the point isn't having humans understand. It's

I agree the tools are not ready because, as you say, the foundational concepts are not yet encoded. But for OP, the point isn't having humans understand. It's having the computer check the proof. You still use traditional journal papers for communicating the proof to humans. You're just also able to say "The proof has been verified and really is true."