Newell, Simon, and Shaw built the Logic Theorist, often called the first artificial intelligence program, which proved theorems from Whitehead and Russell's Principia Mathematica. It famously found a more elegant proof for one theorem than the original. (Developed through 1955-1956; no single agreed calendar day marks its debut, so this date is approximate.)