Formal Mathematics and Proof Assistants - NMMB568
Title: Formal Mathematics and Proof Assistants
Guaranteed by: Department of Algebra (32-KA)
Faculty: Faculty of Mathematics and Physics
Actual: from 2023
Semester: summer
E-Credits: 4
Hours per week, examination: summer s.:2/1, C+Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: not taught
Language: English
Teaching methods: full-time
Teaching methods: full-time
Guarantor: Mgr. Josef Urban, Ph.D.
RNDr. Martin Suda, Ph.D.
Class: M Mgr. MMIB
M Mgr. MMIB > Volitelné
Classification: Mathematics > Algebra
Incompatibility : NMMB566
Interchangeability : NMMB566
Is incompatible with: NMMB566
Is interchangeable with: NMMB566
Opinion survey results   Examination dates   Schedule   Noticeboard   
Annotation -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)
The topic of the course are formal (computer-understandable) mathematics and proof assistants (interactive theorem provers). A proof assistent is a tool to assist with the development of formal proofs by human-machine collaboration. The language of communication is some variant of formal logic and the main aim a high level of assurance that the proven actually holds.We will have a look at the proof assistent Lean, study its theoretical foundations and explore the ways in which it can be used to develop theories, model systems, and prove theorems in computer science as well as mathematics.
Course completion requirements - Czech
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)

Předmět je zakončen ústní zkouškou.

Literature -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)

Blanchette et at. The Hitchhiker's Guide to Logical Verification (available online)

Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean (available online)

Requirements to the exam -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)

Will be specified later.

Syllabus -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (08.12.2022)

We will mostly follow the Hitchhiker's Guide:


  • Definitions and Statements,
  • Backward Proofs, Forward Proofs

(Quantifiers, Connectives, Tactics, Propositions as Types / Proofs as Terms)

Functional–Logic Programming:

  • Functional Programming
  • Inductive Predicates
  • Monads

(Basic Data Structures, Proofs by induction, Arithmetic tactics)

Program Semantics:

  • Operational Semantics
  • Hoare Logic
  • Denotational Semantics

(Small-step/big-step, Partial vs Total correctness, Monotone functions, lattices and



  • Logical Foundations of Mathematics
  • Basic Mathematical Structures
  • Rationals and Real Numbers

(Foundational principles, Subtypes, Quotient types, Type Classes)