Dowodzenie twierdzeń w języku Lean 1000-2M26DTL
Celem przedmiotu jest nauka formalizacji matematyki w języku Lean 4.
1. Podstawowa składnia języka Lean jako języka programowania funkcyjnego.
2. Typy w Lean. Wprowadzenie do teorii typów zależnych.
3. Monady.
4. Równoważność sformułowań/dowodów z typami/wartościami.
5. Indukcyjne konstrukcje.
6. Taktyki.
7. Przegląd biblioteki Mathlib.
8. Przegląd narzędzi sztucznej inteligencji pomocnej w pracy w języku Lean.
Kierunek podstawowy MISMaP
Koordynatorzy przedmiotu
Rodzaj przedmiotu
Wymagania (lista przedmiotów)
Założenia (lista przedmiotów)
Efekty uczenia się
Student zna i rozumie rolę i znaczenie konstrukcji rozumowań matematycznych (K_W02).
Student potrafi konstruować rozumowania matematyczne (K_U01).
Student potrafi analizować pojęcia sformalizowane w wybranych systemach logicznych o znaczeniu informatycznym, tworzyć w nich formalizacje zadanych pojęć bądź też dowodzić niemożności takiej formalizacji (K_U07).
Student jest gotów do krytycznej oceny posiadanej wiedzy i odbieranych treści (K_K01).
Kryteria oceniania
Na ocenę będą składały się: prezentacja pod koniec semestru oraz projekt zaliczeniowy.
Literatura
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/
Więcej informacji
Więcej informacji o poziomie przedmiotu, roku studiów (i/lub semestrze) w którym się odbywa, o rodzaju i liczbie godzin zajęć - szukaj w planach studiów odpowiednich programów. Ten przedmiot jest związany z programami: