Speaker: Yoh Tanimoto (University of Rome, Tor Vergata)

Title: Introduction to Lean theorem prover

Time/Date: 3:00-4:30pm, December 10 (Tue.), 2024

Room: 002 Math Sci Building (It will be also online. The Zoom link is the same as before. If you don't have one, please ask Kawahigashi.)

Abstract: Lean is an interactive theorem prover, which allows one to write mathematical statements and proofs in a programming language and verifies the validity. Writing mathematical proofs in a formal language has a long history, and very recently some of the latest mathematical results have been formalized in Lean. From my own perspective, I will give an overview of its mathematical library mathlib and how to start writing proofs in that language.