There is an embarassingly simple proof that a computer can (in principle) come up with any formal proof that a mathematician can.
The basic components are:
(1) A computer can recognize a proof.
(2) A computer can iterate through every possible sequence of symbols.
For any provable statement
P, we can find a proof with the following algorithm:
For every possible sequence S of symbols:
::: If S is a proof of P, then print S and quit.
Any decidable statement
P can be decided with:
For every possible sequence S of symbols:
::: If S is a proof of P, then print "P is true" and quit.
::: If S is a proof of ~P, then print "P is false" and quit.
And, BTW, humans
do prove things by checking all the cases -- we just usually try very hard to keep the number of cases very small, because we're "lazy".