They date back much further. McCarthy in the 1960s, and over a half dozen groups by 1970, had developed computer assisted proof tools that were proving theorems

They date back much further. McCarthy in the 1960s, and over a half dozen groups by 1970, had developed computer assisted proof tools that were proving theorems. The 4 color theorem in 1976 was just a very famous example. I think Turing (30s? 40s?) and later von Neumann (50s) also did some computer assisted theorem proving, but I’d have to dig for precise references.