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.

Poster

Lectures

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.
Slides, Informal proof of CBS (.pdf), Informal proof of CBS (.tex),
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
Assignment: Partial proof of CBS (.miz), Vocabulary file for CBS (.voc), Hyperlinked version, Hyperlinked version with ATP calls, Video of the Knaster-Tarski proof, First part of the CBS proof.
7th April 2017
Chad E. Brown
HOL Light and its foundations, tactical theorem proving, LCF (small kernel) paradigm. Flyspeck (formal proof of Kepler)
Assignment: Partial Backwards Style Proof of CBS in HOL-light, to be completed by the student, Video of Forward Style Proof of CBS in HOL-light, Video of John Harrison proving CBS in HOL-light.
28th April 2017
Ondřej Kunčar
Isabelle/Isar - an introduction. Combining tactical and declarative styles, automation.
Assignment: Partial Proof of CBS in Isabelle/HOL, to be completed by the student,
12th May 2017
Chad E. Brown
Introduction to Coq and type theory. Curry-Howard isomorphism.
Assignment: Partial proof of CBS in Coq, to be completed by the student, Video of partial proof of CBS in Coq,
26th May 2017
Josef Urban
Further applications, links to modern automated reasoning and AI for mathematics

Resources