Interactive theorem provers are what verifies (or proves) the proof here. This means you don’t even have to look at the actual proof to check its correctness. You just have to make sure the theorem definition is what you wanted (not to say this is trivial) and that no nonsense axioms were defined etc. Now for verifying the theorem prover itself, this is kind of a chicken and the egg problem. We know the mathematical foundations are solid. But to check the implementation of said foundations would require… another theorem prover. In practice, most theorem provers try to make their kernel as small as possible so it can be reasoned about by humans. Coming back to the original topic, mathematics isn’t all proofs though. Someone has to come up with new theories and models. I guess this is what mathematicians would be doing in the future if AI becomes better at proving things than humans. But I could see it narrowing the field, just like it’s doing in others.