Technically, the verification phase does not even require a human anymore with Lean. As long as you believe there are no bugs in Lean (there have been, in the past, so that's a strong caveat), the proof follows from known definitions, axioms, and assumptions. Another caveat is that one can add one's own axioms, so, you'd be able to prove anything if you're not careful and/or dishonest (ouch, maybe yet another reason to be careful with AI-encoded Lean proofs).