LLMs (as well as humans) are algorithms like anything else and so they are also subject to halting problem. I don't see what LLMs do that couldn't be in principle formalized as a Lean tactic. (IMHO LLMs are just learning rules - theorems of some kind of fuzzy logic - and then try to apply them using heuristic search to satisfy the goal. Unfortunately the rules learned are likely not fully consistent and so you get reasoning errors.)