Formal Mathematics and Proof Assistants - NMMB568

• Anglický název: Formal Mathematics and Proof Assistants
• Zajišťuje: Katedra algebry (32-KA)
• Fakulta: Matematicko-fyzikální fakulta
• Platnost: od 2025
• Semestr: letní
• E-Kredity: 4
• Rozsah, examinace: letní s.:2/1, Z+Zk [HT]
• Počet míst: neomezen
• Minimální obsazenost: neomezen
• 4EU+: ne
• Virtuální mobilita / počet míst pro virtuální mobilitu: ne
• Stav předmětu: vyučován
• Jazyk výuky: angličtina
• Způsob výuky: prezenční
• Garant: Mgr. Miroslav Olšák, Ph.D.
• Vyučující: Mgr. Miroslav Olšák, Ph.D.
• Třída: M Mgr. MMIB; M Mgr. MMIB > Volitelné
• Kategorizace předmětu: Matematika > Algebra
• Neslučitelnost : NMMB566
• Záměnnost : NMMB566
• Je neslučitelnost pro: NMMB566
• Je záměnnost pro: NMMB566

Anotace

čeština

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.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Podmínky zakončení předmětu

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

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Literatura

čeština

Stránky předmětu: https://www.olsak.net/mirek/lean-at-matfyz.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)

Poslední úprava: Olšák Miroslav, Mgr., Ph.D. (07.01.2026)

angličtina

Course web page: https://www.olsak.net/mirek/lean-at-matfyz.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)

Poslední úprava: Olšák Miroslav, Mgr., Ph.D. (07.01.2026)

Požadavky ke zkoušce

čeština

Požadavky budou upřesněny.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

angličtina

Will be specified later.

Poslední úprava: Žemlička Jan, doc. Mgr. et Mgr., Ph.D. (08.12.2022)

Sylabus

čeština

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í

Poslední úprava: Olšák Miroslav, Mgr., Ph.D. (28.11.2025)

angličtina

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

Poslední úprava: Olšák Miroslav, Mgr., Ph.D. (28.11.2025)