Is there an automated way to prove really boring elementary number theoretic results?

Solution 1:

You may want to look into the proof assistant Isabelle. It's freely available under a BSD license, and is a start towards the sort of thing your looking for. It's an interactive theorem proving environment that offers a language, Isar, for expressing formal proofs, some built in automated tools, and a sledgehammer tool that will run several external automated theorem provers in parallel. However, I have only just begun to use this system this week, so I am unable to verify for myself if it can handle the simple proof from your question.

This paper outlines the work that went into producing a formally verified proof of the prime number theorem using Isabelle. The authors discuss some of the difficulties they had in proving small lemmas, but they seem confident that the available automated tools will eventually be strong enough to handle these sorts of things. Since this paper was written in 2005, it's conceivable that sufficiently strong tools are available today, but I am unaware of the extent of Isabelle's current capabilities.

Edit: With some coaxing, I was able to produce a partially automated proof of your result using Isabelle. I found it more challenging to get Isabelle to prove this result than to simply prove it myself though. At the moment this probably isn't a practical means of saving labor. Perhaps someone expert in this system with access to a wider library of relevant theorems and lemmas could automate the proofs of a wide class of routine results, but I don't think the functionality you want is quite there yet. Nevertheless, you might find it more fun to try to get a computer to check an apparently routine conjecture than to try to grind through a proof yourself.