alt Hacker Newslean 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
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
there certainly is a relation; you might not be able to prove all the properties you care about because of the halting problem; but that is more a theoretical problem, not a practical one