Room 515, Cosmology Building, NTU
(臺灣大學次震宇宙館 515研討室)
Formalizing Calculus Theorems in Lean: A Gentle Introduction
Hsin-Po Wang (National Taiwan University)
Abstract
In this talk, we will demonstrate how to formalize and verify theorems from elementary calculus using the Lean theorem prover. Starting from classical results such as the Mean Value Theorem, we will illustrate how Lean can rigorously check each step of a mathematical proof. The talk aims to give the audience an accessible introduction to interactive theorem proving, showing how formal tools like Lean can assist in developing fully verified mathematics.
Meeting number (access code): 2517 269 5198
Meeting password: 2iV2hF2F8YX
Organizer: Mao-Pei Tsui (NTU)
