Automated proof of ring commutativity problems by algebraic methods

Using a simple computer program, we have proved thousands and thousands of instances ofthe theorem that for any integer n>1, for any element x in an associative ring, xn=x implies the commutativity of the ring (an instance of the theorem is obtained by taking a specific value for n). The program is based on Newton's binomial theorem and Euclid's gcd algorithm. New algorithms are introduced to speed up the gcd computation and to decide quickly whether a binomial coefficient is odd