Recorded 13 February 2023. John Harrison of Amazon Web Services presents "Formalization and Automated Reasoning: A Personal and Historical Perspective" at IPAM's Machine Assisted Proofs Workshop. Abstract: 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. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/