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 2025
• 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: taught
• Language: English
• Teaching methods: full-time
• Guarantor: Mgr. Miroslav Olšák, Ph.D.
• Teacher(s): Mgr. Miroslav Olšák, 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

Annotation

English

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.

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

Course completion requirements

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

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

Literature

English

Course web page: https://www.olsak.net/mirek/lean-lecture.html

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)

Last update: Olšák Miroslav, Mgr., Ph.D. (14.02.2026)

Czech

Stránky předmětu: https://www.olsak.net/mirek/lean-lecture.html

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)

Last update: Olšák Miroslav, Mgr., Ph.D. (14.02.2026)

Requirements to the exam

English

Will be specified later.

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

Czech

Požadavky budou upřesněny.

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

Syllabus

English

Basics

• data structures

• inductive types

• recursive functions

• propositions, quantification

Theory

• dependent types

• propositions as types

• link to set theory, universes

• equality kinds: syntactic, definitional, relational (provable)

• typeclass search

Proving

• tactics (manipulating goal, manipulating context, massaging, bashing, ...)

• library search

• mathematical koncepts (numbers, algebra, analysis, ...)

• program termination

If we have time

• AI tools

• metaprogramming

Last update: Olšák Miroslav, Mgr., Ph.D. (28.11.2025)

Czech

Základy

• datové struktury

• induktivní typy

• rekurzivní funkce

• výroky, kvantifikace

Teorie

• závislé typy

• výroky jako typy

• souvislost s teorií množin, univerza

• typy rovnosti: syntaktická / definiční / relační (dokazatelná)

• typové třídy (typeclass)

Dokazování

• taktiky (krok od cíle, krok od přepokladů, ladící, mlátící)

• vyhledávání v knihovně

• matematické koncepty (čísla, algebra, analýza, ...)

• konečnost programů

Když zbude čas

• AI nástroje

• metaprogramování

Last update: Olšák Miroslav, Mgr., Ph.D. (28.11.2025)