Of course we all remember that discovering new theorems in mathematics and new _proofs_ of theorems in mathematics has been done to death since the beginnings o

Of course we all remember that discovering new theorems in mathematics and new _proofs_ of theorems in mathematics has been done to death since the beginnings of AI. For example, see the wikipedia page on the Automated Mathematician (1977): https://en.wikipedia.org/wiki/Automated_Mathematician https://en.wikipedia.org/wiki/Automated_Mathematician And follow the links from that article to (stub) articles on HR (2016): https://en.wikipedia.org/wiki/HR_(software) https://en.wikipedia.org/wiki/HR_(software) And Graffiti (1989): https://en.wikipedia.org/wiki/Graffiti_(program) https://en.wikipedia.org/wiki/Graffiti_(program) And then jump over to the Automated Theorem Proving article: https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving And from there to the article on the Logic Theorist (1956): https://en.wikipedia.org/wiki/Logic_Theorist https://en.wikipedia.org/wiki/Logic_Theorist Which, I quote from the wikipedia article: Logic Theorist is a computer program written in 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw.[1] It was the first program deliberately engineered to perform automated reasoning and is called "the first artificial intelligence program".[a] It would eventually prove 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some.[3]