Comment on Theories on Theories
lemonwood@lemmy.ml 16 hours agoLean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
Comment on Theories on Theories
lemonwood@lemmy.ml 16 hours agoLean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
pfried@reddthat.com 15 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.