Earlier quoted context omitted.
Only if they can understand the proofs first. However, LLMs aren't capable of writing proofs. They can only regurgitate text that looks like a proof by training on proofs already written. There's no reasoning behind what they produce. So why waste the time of a human to review it? If the provers' kernel and automation make the proof pass but it makes no sense, what use is it? People write proofs to make arguments to…
If the proof make it past the validation it’s a valid proof and makes sense by definition.
It means your proof proves something.
Whether it's something you care about, or even something that should be true at all is out of scope.