[MatthiasPortzel]

> But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.

Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.

But the halting problem, and the Collatz conjecture, and all mathematical truth, is fundamentally embedded inside of systems of formal logic. Gödel's Incompleteness Theorem doesn't say anything about systems of truth outside of formal mathematical logic. So this result isn't relevant to Physics, for example.

However, Gödel's Theorem, and this proof, don't rely on any particular qualities of the formal system, other than the ability to enumerate proofs (and other things that we think of as inherit to logic). So this proof applies not just to Lean, but also to every method of proving things in math.

[lmm]

> Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.

This is wrong - see Dyson's eternal intelligence.