Consider the assertion:

There is no completely multiplicative function $f:\mathbb{N}\rightarrow {\pm 1}$ with $\left|\sum_{n\leq x}f(n)\right|\leq 2$ for all $x\geq 0$.

One can write a very short program to show that things go wrong for $x\geq 247.$ Doing this by hand with current technology requires an unmanagable amount of cases (cf. http://michaelnielsen.org/polymath1/index.php?title=Human_proof_that_completely_multiplicative_sequences_have_discrepancy_greater_than_2). I wonder whether you have encountered similar situations. I am aware that one can always construct artificial examples. That is not what I want. Rather that you consider some special case of a theorem you try to prove, such that you can prove this with a computer, but not by hand.

Btw. a short proof of the above would also count as an answer.