The Program That Proved Theorems Before AI Had a Name
Months before the Dartmouth Conference coined 'artificial intelligence,' the Logic Theorist became the first program to autonomously prove mathematical theorems — and one of its proofs was more elegant than the human original.
Paolo Massa / Public domain
Over Christmas, Allen Newell and I invented a thinking machine.
— Herbert A. Simon
In 1955, before the term “artificial intelligence” was coined, Allen Newell, Herbert A. Simon, and Cliff Shaw developed the Logic Theorist, a pioneering program that proved mathematical theorems.
What happened: In 1955, Allen Newell, Herbert A. Simon, and Cliff Shaw created the Logic Theorist, a program designed to prove theorems from Whitehead and Russell’s Principia Mathematica. The program successfully proved 38 of the first 52 theorems in the book, including finding a shorter proof for Theorem 2.85 than the original. 1
Why it matters: The Logic Theorist marked a significant milestone in the history of AI, establishing the paradigm of symbolic reasoning and automated theorem proving. Its success inspired further research and development in the field, leading to more advanced AI systems like the General Problem Solver. Newell and Simon’s contributions were recognized with the Turing Award. 2, 3
Further reading:
Why This Mattered
The Logic Theorist proved 38 of the first 52 theorems in Russell and Whitehead's Principia Mathematica, and its proof of Theorem 2.85 was shorter and more elegant than the original. It established the paradigm of AI as symbolic reasoning and inspired the entire field of automated theorem proving. Newell and Simon would go on to develop the General Problem Solver and win the Turing Award.
