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

▲

auggierose 4 hours ago | parent [-]

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

	▲	gf000 4 hours ago \| parent [-]
		> you might not be able to prove all the properties you care about And just to add, this is also true of "human" mathematics as well.