3 ms·
No. Anyone that's tried to use a state-of-the-art automated theorem prover (like ACL2) knows we have a long, long way to go. They're still pretty dumb. That
by mattmight 16y ago
No.
Anyone that's tried to use a state-of-the-art automated theorem prover (like ACL2) knows we have a long, long way to go.
They're still pretty dumb.
That said, I'm convinced that Godels Incompleteness Theorems hold only in the limit -- the majority of propositions of human interest are probably amenable to mechanical proving.