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)?
$\begingroup$
$\endgroup$
4
-
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$– ConifoldFeb 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$– Mauro ALLEGRANZAFeb 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$– Carl WitthoftFeb 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$– Timothy ChowJul 13, 2021 at 18:18
Add a comment
|