Mathematics
AI in proof, conjecture, symbolic reasoning and optimisation.
3 milestones
AM: Automated Mathematician Developed by Douglas Lenat
In 1976, Douglas Lenat at Stanford University completed AM (Automated Mathematician), a heuristic program that explored elementary mathematics by modifying and combining LISP-coded concepts, discovering properties such as prime numbers without being explicitly programmed to do so.
James Slagle Completes SAINT: A Symbolic Automatic Integrator
In 1961, James R. Slagle at MIT completed SAINT (Symbolic Automatic INTegrator), a heuristic program that solved indefinite integration problems at the level of a first-year calculus student, demonstrating that symbolic mathematical reasoning could be encoded in a computer program.
The Logic Theorist: first automatic theorem-proving program, developed by Newell, Shaw, and Simon
In late 1955, Allen Newell, J. Clifford Shaw, and Herbert A. Simon at RAND Corporation and Carnegie Institute of Technology completed the Logic Theorist, a computer program that proved mathematical theorems from Whitehead and Russell's Principia Mathematica by heuristic search, establishing that symbolic reasoning could be mechanised.