LEAN -- důkazy pomocí počítače - NTIN115
| Anglický název: |
LEAN – Computer-Assisted Proofs |
| Zajišťuje: |
Informatický ústav Univerzity Karlovy (32-IUUK) |
| Fakulta: |
Matematicko-fyzikální fakulta |
| Platnost: |
od 2025 |
| Semestr: |
zimní |
| E-Kredity: |
5 |
| Rozsah, examinace: |
zimní s.:2/2, 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í |
|
|
| Anotace -
| |
|
Používání interaktivního dokazovacího systému LEAN.
Poslední úprava: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)
Using the interactive proof assistant LEAN.
Poslední úprava: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)
|
| Podmínky zakončení předmětu -
| |
|
Cvičení probíhá formou domácích úkolů. Zápočet je udělen za vyřešení dostatečného počtu úkolů.
Zkouška je za zapsání rozsáhlejšího důkazu pomocí LEANu a následnou diskuzi nad tímto důkazem.
Poslední úprava: Šámal Robert, doc. Mgr., Ph.D. (06.10.2025)
Exercises in the form of homework assignments. Credit is awarded for solving a sufficient number of problems.
The exam is for writing a more extensive proof using LEAN and a follow-up discussion about the proof.
Poslední úprava: Šámal Robert, doc. Mgr., Ph.D. (06.10.2025)
|
| Literatura -
| |
|
Bhavik Mehta: Formalising Mathematics
https://github.com/b-mehta/formalising-mathematics-notes
Jeremy Avigad: Mathematics in LEAN
https://leanprover-community.github.io/mathematics_in_lean/
https://lean-lang.org/publications/
Poslední úprava: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)
Bhavik Mehta: Formalising Mathematics
https://github.com/b-mehta/formalising-mathematics-notes
Jeremy Avigad: Mathematics in LEAN
https://leanprover-community.github.io/mathematics_in_lean/
https://lean-lang.org/publications/
Poslední úprava: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)
|
| Sylabus -
| |
|
- použití systému LEAN na příkladech známých/blízkých studentům bakalářského studia
- důraz na snadné a intuitivní použití
- ukázky z lineární algebry, teorie čísel, analýzy i diskrétní matematiky
- - metaprogramování (rozšiřování systému o automatické dokazovací postupy)
- - pokročilé současné věty verifikované pomocí LEANu
- - ukázky použití strojového učení
Poslední úprava: Šámal Robert, doc. Mgr., Ph.D. (05.09.2025)
- Using the LEAN system on examples familiar to bachelor students
- Emphasis on ease and intuitive use
- Examples from linear algebra, number theory, analysis, and discrete mathematics
- Depending on interest, also:
- - Metaprogramming (extending the system with new automated proving procedures)
- - Advanced recent theorems verified using LEAN
- - Demonstrations of machine learning applications
Poslední úprava: Šámal Robert, doc. Mgr., Ph.D. (05.09.2025)
|
