(in Polish) Dowodzenie twierdzeń w języku Lean 1000-2M26DTL
The goal of the course is to learn how to formalize mathematics in Lean 4.
1. Basic syntax of Lean as a functional programming language.
2. Types in Lean. Introduction to Dependent Type Theory.
3. Monads.
4. Equivalence of statements/proofs and types/values.
5. Inductive constructions.
6. Tactics.
7. Overview of Mathlib.
8. Overview of AI tools useful when working with Lean.
Main fields of studies for MISMaP
Course coordinators
Type of course
Requirements
Prerequisites
Assessment criteria
The grade will depend on: a presentation near the end of the semester and a programming project.
Bibliography
https://lean-lang.org/doc/reference/latest/
https://docs.lean-lang.org/lean4/doc/whatIsLean.html
https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html
https://leanprover-community.github.io/lean4-metaprogramming-book/main/01_intro.html
https://browncs1951x.github.io/static/files/hitchhikersguide.pdf
https://perfect-math-class.leni.sh/
Additional information
Information on level of this course, year of study and semester when the course unit is delivered, types and amount of class hours - can be found in course structure diagrams of apropriate study programmes. This course is related to the following study programmes: