The proofs could be optimized for human consumption. OpenAI could optimize each proof for fewest theorems, low branching, or short dependency chains. OpenAI could have an adversarial network enforce that proofs look human. OpenAI could spend a couple more machine hours per paper with the prompt "edit for clarity".