Formalization and Automated Reasoning: A Personal and Historical Perspective

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.

Syllabus

Intro
Summary of talk
A personal retrospective
Automation, interaction, libraries
Automated theorem proving in its pomp
First steps in interactive theorem proving
Three influential proof checkers
Milner on automation and interaction
Reasons for developing library results
Libraries: what can go wrong?
The Great 100 Theorems
The Isoperimetric Theorem (formally)
Unpacking the definitions (standard)
Unpacking the definitions (not so standard)
Jordan with inside and outside
Reduction to the convex case (informally)
Reduction to the convex case (formally)
Steiner's hinge argument (informally)
Existence of maximal curve
The hinge gets stuck
Osserman's analytical proof (1)
Formalizing Osserman's proof
Wirtinger's inequality (informally)
Keeping the calculus general
The overall isoperimetric proof
The final statement