Formal Mathematics and Proof Assistants (Spring 2017)

The course takes place on Friday mornings (9:50 to 13:00) in room K6 at MFF UK, Sokolovská 83, Prague 8.

The course will introduce formal (computer-understandable) mathematics and proof assistants (interactive theorem provers). Several mainstream systems such as HOL, Isabelle, Mizar and Coq will be introduced, together with their foundations. We will give an overview of recent major formalization projects, such as the formal proof of the Kepler conjecture in HOL Light, and show applications in software verification. We will also discuss wider motivation, such as the QED Manifesto, and links to modern automated reasoning and artificial intelligence systems for mathematics.



3rd March 2017
Josef Urban and Chad E. Brown
Introduction, history, QED Manifesto, overview of foundations and proof styles, automated vs. interactive theorem proving. Informal proof of Cantor-Bernstein-Schroeder (CBS) used as a formalization example.
17th March 2017
Josef Urban
Mizar - an introduction. Declarative proof style, ZFC, natural-language features, proof checking, links to automated theorem proving. Formalization of the CBS theorem.
Mizar installation packages for version 5.29.1227: Linux , Windows
Installation instructions: Linux, Windows
7th April 2017
Chad E. Brown
HOL Light and its foundations, tactical theorem proving, LCF (small kernel) paradigm. Flyspeck (formal proof of Kepler)
28th April 2017
Ondřej Kunčar
Isabelle/Isar - an introduction. Combining tactical and declarative styles, automation.
12th May 2017
Chad E. Brown
Introduction to Coq and type theory. Curry-Howard isomorphism.
26th May 2017
Josef Urban
Further applications, links to modern automated reasoning and AI for mathematics