LEAN – Computer-Assisted Proofs - NTIN115

• Title: LEAN -- důkazy pomocí počítače
• Guaranteed by: Computer Science Institute of Charles University (32-IUUK)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2025
• Semester: winter
• E-Credits: 5
• Hours per week, examination: winter s.:2/2, 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: doc. Mgr. Robert Šámal, Ph.D.
• Teacher(s): doc. Mgr. Robert Šámal, Ph.D.

Annotation

English

Using the interactive proof assistant LEAN.

Last update: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)

Czech

Používání interaktivního dokazovacího systému LEAN.

Last update: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)

Course completion requirements

English

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.

Last update: Šámal Robert, doc. Mgr., Ph.D. (06.10.2025)

Czech

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.

Last update: Šámal Robert, doc. Mgr., Ph.D. (06.10.2025)

Literature

English

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/

Last update: Pangrác Ondřej, RNDr., Ph.D. (16.05.2025)

Syllabus

English

• 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

Last update: Šámal Robert, doc. Mgr., Ph.D. (05.09.2025)

Czech

• 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

• podle zájmu též

• - 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í

Last update: Šámal Robert, doc. Mgr., Ph.D. (05.09.2025)