Introduzione alla formalizzazione di matematica in Lean

Introduzione alla formalizzazione di matematica in Lean, corso di dottorato in Matematica

Ricevimento: su appuntamento (e-mail: hoyt at_mark mat.uniroma2.it)
2025/2026 Primo semestre, dal 10 Dicembre
Descrizione del corso, orario: Mer 9:30-11:30, Gio 9:30-11:30, Aula Dal Passo (fino alla lezione 9)

Testi/fonti consultabili:

Jeremy Avigad, Patrick Massot Mathematics in Lean
Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich Theorem proving in Lean 4
Heather Macbeth The mechanics of proof
Jeremy Avigad, Joseph Hua, Robert Y. Lewis, and Floris van Doorn Logic and proof

Programma:

Dependent type theory, implenentazione in Lean
Tactics di base e avanzati
Teoria di insiemi, funzioni, numeri reali in Lean
Structure, esempi (tipi e operazioni algebriche)
Gerarchia di strutture, esempi (magma, monoido, semigruppo, gruppo)
Esempi concreti di strutture avanzate
Dimostrazioni automatizzate, creare un proprio progetto, modalit\`a per contribuire a mathlib.

Diario (piano) delle lezioni:

11/19 (Riunione preliminare) Installazione di VS Code con estensioni, Git, Curl, clone di reposotori. slides
12/10 Introduzione a Lean, motivazione per formalizzazione, differenza da computer algebra system e ATP, dimostrazioni formali, vantaggi di matematica formalizzata, esercizi. slides
12/11 Logic of Lean
12/17 Basic tactics
12/18 Real numbers
2026/01/07 Sets and functions
2026/01/08 Structures
2026/01/14 Hierarchy of structures
2026/01/15 Magmas, monoids, semigroups and groups
2026/01/21 More advanced structures
2026/01/?? Advanced topics

Pagina principale di Yoh Tanimoto