This might sound pedantic but it is worth being precise here. These kind of issues are either "Proving the wrong statements" or "using dubious axioms". Both of these are issues not issues of the proof. You do not need to understand the proof term to identify such issues nor do you need to understand the proof term to verify their absence.

I am not saying that LEAN proofs are without issues. What I am trying to say is that the proof term itself is not the trusted part.

To be convinced of a proof, an expert will have to (1) review the definitions, (2) review the axioms, and (3) trust the kernel.

Issues can arise in all 3 but the proof itself is untrusted.

Definitions in a formal language are hard and error prone. Axioms are mostly not an issue. Most LEAN proofs should only make use of the three standard axioms (Choice, Propext, and Quotient soundness) and it is well studied what these axioms mean. Actual bugs happen in 3. Kernel bugs can for example mean that the kernel incorrectly checks a proof of "False". Kernel bugs do happen but there are measures against it (e.g., using multiple kernels to check your proof) and it is quite rare for a human to accidentally trigger one. LLMs have accidentally triggered kernel bugs in the past.

They should be fixed?