The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html