As a small-scale example of this, see the book "A=B".

http://www.math.upenn.edu/~wilf/AeqB.html

The authors reduce the proving of a wide class of combinatorial identities, which were formerly regarded as extremely nontrivial, to a mechanical calculation. This has been implemented in Maple. Input your favorite identity, push the button, and watch the computer spit out a proof.