From a lot of googling, it seems like the answer might be "Mizar", but I am not completely sure.

What was (or is?) the first automated theorem prover (i.e. not necessarily active right now)?

  • 4
    $\begingroup$ It isn't Mizar (1973). Wikipedia's history section lists implementations already from 1950-s, like Davis's program (1953) and Logic Theory Machine (1956). $\endgroup$
    – Conifold
    Feb 24, 2021 at 20:58
  • 2
    $\begingroup$ Also relevant Hao Wang result of 1959: "In 1959, Wang wrote on an IBM 704 computer a program that in only 9 minutes mechanically proved several hundred mathematical logic theorems in Whitehead and Russell's Principia Mathematica." See Toward mechanical mathematics (1960) $\endgroup$ Feb 25, 2021 at 9:21
  • 2
    $\begingroup$ This question might be a bit broad,as any conjecture which can be proved is a theorem; many are pathologically trivial. Could you try to limit it to certain "levels" of theorems, perhaps? $\endgroup$ Feb 25, 2021 at 12:57
  • $\begingroup$ A good reference is The Automation of Proof: A Historical and Sociological Exploration by Donald Mackenzie, IEEE Annals of the History of Computing, Vol. 17, No. 3 (1995), 7-29. $\endgroup$ Jul 13, 2021 at 18:18


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.