Bounded proof search is NP-complete, and you can see this if you imagine transforming a bounded proof search into a satisfiability problem; go from "what, if an

Bounded proof search is NP-complete, and you can see this if you imagine transforming a bounded proof search into a satisfiability problem; go from "what, if any, proof starts at these assumptions and reaches these conclusions in less than N steps?" into "what, if any, assignment of Boolean values will encode a proof in O(N) values?" This is precisely what got both Gödel and Nash interested in what would become P vs NP. Computers beating humans at chess is a great example of not being smarter, but being stupid faster. Both humans and computers approach PSPACE-complete problems like chess by approximating their searches and looking at trees of possible moves. We have no special insights into how to consider or evaluate moves; we have psychological profiles on which moves might be connected during practical play but no reason to require people to make such moves, and those profiles are largely limited to "openings", classifying the relatively few initial trees. How do computers beat humans in chess? They do exactly what we do, but faster. This isn't smart, but fast stupid.