Comment on Theories on Theories
pfried@reddthat.com 17 hours 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 17 hours agoIt is not necessary to solve the halting problem to show that a particular proof is correct.
lemonwood@lemmy.ml 17 hours 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 17 hours 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.