Completed
Intro
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Formalization and Automated Reasoning: A Personal and Historical Perspective
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Summary of talk
- 3 A personal retrospective
- 4 Automation, interaction, libraries
- 5 Automated theorem proving in its pomp
- 6 First steps in interactive theorem proving
- 7 Three influential proof checkers
- 8 Milner on automation and interaction
- 9 Reasons for developing library results
- 10 Libraries: what can go wrong?
- 11 The Great 100 Theorems
- 12 The Isoperimetric Theorem (formally)
- 13 Unpacking the definitions (standard)
- 14 Unpacking the definitions (not so standard)
- 15 Jordan with inside and outside
- 16 Reduction to the convex case (informally)
- 17 Reduction to the convex case (formally)
- 18 Steiner's hinge argument (informally)
- 19 Existence of maximal curve
- 20 The hinge gets stuck
- 21 Osserman's analytical proof (1)
- 22 Formalizing Osserman's proof
- 23 Wirtinger's inequality (informally)
- 24 Keeping the calculus general
- 25 The overall isoperimetric proof
- 26 The final statement
