Tuesday, February 24, 2026 2:00 pm
-
3:00 pm
EST (GMT -05:00)
Frédéric Dupuis, University of Montreal
A brief introduction to the Lean theorem prover
Frédéric Dupuis, University of Montreal
Lean is an interactive theorem prover: a programming language that can be used to formalize mathematical proofs. The compiler then checks that the proof provided is indeed correct. In this talk, I will give a quick introduction to Lean for interested mathematicians/physicists/computer scientists hoping to one day be able to formalize their research results in this way.
Location
QNC 0101