The Logic Theorist
The Logic Theorist, the first expert system, was used to prove mathematical theorems. It was able to recreate many theorems already found by human mathematicians and in one instance was able to come up with a more elegant proof than the one devised by human mathematicians.
