Seminar of the Department of Algebra and Geometry - Viera Glevitzká (16.10.2026)

Friday 16.10.2026 at 13:30, Lecture room F2

13. 10. 2026 08.41 hod.
By: Tibor Macko

Viera Glevitzká:
The Snake Lemma (An example of a formalization of mathematics in LEAN)

Abstract:
We explain the basics of formalization of mathematics in the programming language LEAN 4. We illustrate it through the statement and proof of the so-called Snake lemma from algebra which was done in our bachelor thesis. The mathematical part only assumes basic knowledge of algebra from any first-year linear algebra course, and no knowledge of programming is assumed.