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)?

  • 3
    $\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$ – Mauro ALLEGRANZA 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$ – Carl Witthoft Feb 25 at 12:57

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.