Comment by IshKebab

Computers are much much better at all that stuff than almost everyone too. Try asking Wolfram Alpha to solve something. Computers have gotten really good at proving things in the last couple of decades and formal verification methods are becoming increasingly popular.

I think sharemywin is probably on to something. It's going to be really hard for an AI to prove that e.g. x>0 && x+y <= 1 && y>1 is unsatisfiable, but it's trivial for an SMT solver. On the other hand it probably isn't that much of a leap to make an AI that can feed that problem into an SMT solver.