Harrison, “Formalization and Automated Reasoning: A Personal and Historical Perspective”
I finally found a (version of) recording of a talk by John Harrison about the history of provers and working with formal mathematics, where he discusses the idea that automated proving was a backward step, and the industry should have started with proof assistants.