In this talk I will try to first place the recent interest in
machine-assisted proof in its historical perspective, discussing
early work in the field and tracing the development of some
of the current research themes. I will then try to identify
some lessons, partly from my own experience, and also note where
I see fruitful paths to explore in the future.