Seminari del Dipartimento di Matematica

Seminario del 2025

Lorenzo Luccioli

Introduction to Mathematical Formalization with Lean 4 (Part 1)

nel ciclo di seminari: INTRODUCTION TO MATHEMATICAL FORMALIZATION WITH LEAN 4

SEMINARIO INTERDISCIPLINARE

Mathematical formalization has attracted increasing attention in recent years, with Lean 4 emerging as one of the central tools in this area. This series of four seminars will introduce mathematical formalization, discuss its significance, and showcase recent examples of successful formalization projects. Two of the seminars will provide hands-on tutorials using the interactive theorem prover Lean 4. In the final seminar, we will examine how artificial intelligence and formalization interact, highlighting recent developments in autoformalization and automatic theorem proving.