Reasoning, Proof, and Formalization with Lean 4
A Gentle Introduction to Lean for Beginners
Lecture notes, slide, file Lean per la lezione in classe, esercizi e soluzioni.
Prossime lezioni
- Lunedì 19 ottobre 2026, 16:00–17:30
Materiali per lezione
Lezione 1Lezione 1: Che cos'è un interactive theorem prover?Apri i materialiLezione 2Lezione 2: Proposizioni, dimostrazioni e regole logicheApri i materialiLezione 3Lezione 3: Dalla deduzione naturale alle dimostrazioni in LeanApri i materialiLezione 4Lezione 4: Logica classica e quantificatoriApri i materialiLezione 5Lezione 5: Regole dei quantificatoriApri i materialiLezione 6Lezione 6: Tipi induttivi, ricorsione e induzioneApri i materialiLezione 7Lezione 7: Induzione, semplificazione e verifica del softwareApri i materiali