Hi all,

Next Tuesday, our visitor Frédéric Dupuis will talk about “A brief introduction to the Lean theorem prover”. See below for the abstract. The talk will take place on Tuesday at 11:15 in HIT E41.1

Best, Ladina

%%%%%%

Title: A brief introduction to the Lean theorem prover

Abstract: 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.