As others in this thread have pointed out, some of those proofs involve calls to high-power decision procedures, so I was curious to see if as a baseline, could Z3 solve the problems in the blog post with no guidance?

For 5/6 of the problems, Z3 solves them automatically and instantly, with the same problem encoding as the problems in the post. (Problem 2 involves factorial, so that one can't be straightforwardly translated to Z3.)

Code: https://gist.github.com/anishathalye/0d5cd359adcde85fac6bf76...