> inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).