Seminár Katedry algebry a geometrie - Viera Glevitzká (16.10.2026)

v piatok 16.10.2026 o 13:30 hod. v posluchárni F2

13. 10. 2026 08.34 hod.
Od: Tibor Macko

Prednášajúci: Viera Glevitzká

Názov: The Snake Lemma (An example of a formalization of mathematics in LEAN)

Termín: 16.10.2026, 13:30 hod., poslucháreň F2

Abstrakt:
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.