The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.

If I understand correctly, the only thing you need to do for correctness is express your axioms and your theorems faithfully. For standard purposes, I assume most of the axioms you want to use are prior art and can be easily reused.

These axioms don’t have to be the core axioms of math. If some other result has been formally proven, I presume you can simply use that result as an axiom.

As long as you do those things, what happens in between is immaterial from a correctness point of view because each of those statements is proved by the statements before them.

Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

How do you know that what a human says they formalized is actually formalized?