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)?
History of Science and Mathematics Stack Exchange is a question and answer site for people interested in the history and origins of science and mathematics. It only takes a minute to sign up.Sign up to join this community