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 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 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 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 at 18:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.