Comment on Theories on Theories
pfried@reddthat.com 2 months agoIt is not necessary to solve the halting problem to show that a particular proof is correct.
Comment on Theories on Theories
pfried@reddthat.com 2 months agoIt is not necessary to solve the halting problem to show that a particular proof is correct.
lemonwood@lemmy.ml 2 months ago
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
pfried@reddthat.com 2 months ago
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that Lean is Turing complete does not prevent it from verifying the proofs that it has verified.
lemonwood@lemmy.ml 2 months ago
It’s not about those specific proofs. You’re claiming, that every possible proof stated in lean will always halt. Lean tries to evade the halting problem best as possible, by requiring functions to terminate before it runs a proof. But it’s not able to determine for every lean program it halts or not. That would solve the halting problem. Furthermore, the kernel still relies on CPU, memory and OS behavior to be bug free. Can you be sure enough in practice, yeah probably. But you’re claiming absolute metaphysical certainty that abolishes the need for philosophy and sorry, but no software will ever achieve that.
pfried@reddthat.com 2 months ago
It certainly is about those specific proofs and anything that has been rigorously proven in Lean. We’re discussing techniques that show something is correct forever, and those proofs show that something is correct forever. Philosophical arguments don’t even show that something is correct today.
Only to a point, just like human language proofs require the reviewers brains to be bug free to a point. The repeated verification makes proofs as correct as anything can get.