SubjectsSubjects(version: 945)
Course, academic year 2023/2024
   Login via CAS
Formal Mathematics and Proof Assistants - NMMB566
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: 3
Hours per week, examination: summer s.:2/0, Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: not taught
Language: English, Czech
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 : NMMB568
Interchangeability : NMMB568
Is incompatible with: NMMB568
Is interchangeable with: NMMB568
Annotation -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (02.01.2024)
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.
Course completion requirements - Czech
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)

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

Literature -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (07.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. (21.05.2021)

Will be specified later.

Syllabus -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (01.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)

Charles University | Information system of Charles University |