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.

Halting problem only stops you from your prover from working on all programs.

On some programs like "stop" or "while(true)" the proof is easy.

With more sophisticated analysers it becomes possible on wider range of programs.

Dijkstra's approach would be to prove there is a strictly decreasing natural number associated to the loop.

This limits programs to the ones that can be formally shown to terminate. Which is good enough for most purposes.

My approach is to accept programs that run forever as long as I'm fairly sure each loop makes progress of some sort (instead of simply doing "while not solved: continue").

Edit: There's also a fun algorithm that, as far as I know, only provably terminates by being bounded by a sequence of strictly decreasing ordinals. Which breaks all kinds of models for proving it terminates.

The same way Goedel's 0th incompleteness theorem doesn't make math proofs impossible (this is not sarcasm btw).

do you mean how is halting problem not a blocker or how halting problem itself is proven?

answer to the first is same as always - by simply not guaranteeing that everything is provable, especially in finite amount of time

lean has no relation to the halting problem; you can think of it as a language that allows proofs to be encoded as code, and the compiler that runs that code as knowing how to enforce mathematical constraints appropriately