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 takes place on Friday mornings (9:50 to 13:00) in room K6 at MFF UK, Sokolovská 83, Prague 8.
3rd March 2017

Introduction, history, QED Manifesto, overview of foundations and
proof styles, automated vs. interactive theorem proving. Informal proof of CantorBernsteinSchroeder (CBS) used as a formalization example.

17th March 2017

Mizar  an introduction. Declarative proof style, ZFC, naturallanguage features, proof checking, links to automated theorem proving. Formalization of the CBS theorem.

7th April 2017

HOL Light and its foundations, tactical theorem proving, LCF (small
kernel) paradigm. Flyspeck (formal proof of Kepler)

28th April 2017

Isabelle/Isar  an introduction. Combining tactical and declarative styles, automation.

12th May 2017

Introduction to Coq and type theory. CurryHoward isomorphism.

26th May 2017

Further applications, links to modern automated reasoning and AI for mathematics
