Solving the halting problem means writing a program which can tell whether an arbitrary other program will halt or not.

Proving that a particular program will or won't halt can still be easy.

The halting problem does imply that there exist programs which are entirely correct that lean will never be able to prove the correctness of, but this is not really relevant in practice.