As a small-scale example of this, see the book "A=B". http://www.math.upenn.edu/~wilf/AeqB.html http://www.math.upenn.edu/~wilf/AeqB.html The authors reduce t

As a small-scale example of this, see the book "A=B". http://www.math.upenn.edu/~wilf/AeqB.html 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.