The problem is that there will be far more formally verified proofs than that human mathematicians around the world can read, much less explain. What then? Would the role of mathematicians just become explainers of AI generated proofs?