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)?
Asked
Active
Viewed 111 times
7
-
4It isn't Mizar (1973). Wikipedia's history section lists implementations already from 1950-s, like Davis's program (1953) and Logic Theory Machine (1956). – Conifold Feb 24 '21 at 20:58
-
2Also 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) – Mauro ALLEGRANZA Feb 25 '21 at 09:21
-
2This 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? – Carl Witthoft Feb 25 '21 at 12:57
-
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. – Timothy Chow Jul 13 '21 at 18:18