Google, IBM & Meta Certificates — All 10,000+ Courses at 40% Off
One annual plan covers every course and certificate on Coursera. 40% off for a limited time.
Get Full Access
Explore a comprehensive lecture on the history and development of machine-assisted proofs in mathematics and computer science. Delve into John Harrison's personal experiences and insights as he traces the evolution of automated reasoning from its early beginnings to current research themes. Gain valuable perspectives on the interplay between automation, interaction, and libraries in theorem proving. Examine the development of influential proof checkers and their impact on the field. Investigate the challenges and opportunities in building mathematical libraries, including a detailed exploration of the formalization of the Isoperimetric Theorem. Learn about various proof techniques, from Steiner's hinge argument to Osserman's analytical approach, and understand how they are implemented in formal systems. Discover potential future directions for research in machine-assisted proofs and automated reasoning.
