Unless the proofs themselves are defined with natural language, I don't see them being adopted by humans. It takes a high cognitive load to read let alone write a proof.
Look at the guy whose AI changed the entire rules of the game to avoid breaking the law. Was that really the desired outcome? And the more you try to lock it down the more language you add and therefore more ambiguity and assumptions.
You cannot solve the problems of language with more language.