Things have moved on since then, as artificial intelligence has started being used in formalisation, [...]
With how AI works fundamentally, wouldn't you still need to verify the results generated by AI? Doesn't seem like an applicable field for it, at least in its current state.
I don't think trusting the Lean kernel is enough: you also need to trust that all of the Lean code is a valid translation of the informal proof. Given that the informal proof is already gigantic, and that there is no general mechanical way to verify if a formal statement corresponds 1:1 with an informal statement, it's far from trivial to trust that the Lean representation of the proof is the same thing as the original proof.
Now, if the proof works, presumably this problem goes away: Lean can show that based on this proof, the original statement holds. But if Lean says that this formal proof doesn't work, that doesn't tell you anything about the informal proof: the error may only be in the formalization.
Agreed; translating to Lean/Coq is more likely to prove the positive rather than the negative. It may still be useful in pinpointing where incorrect proofs go wrong.
With how AI works fundamentally, wouldn't you still need to verify the results generated by AI? Doesn't seem like an applicable field for it, at least in its current state.