Getting started with the Lean theorem prover

Thursday, October 26, 2017 - 13:00
427 Thackeray Hall

Abstract or Additional Information

Lean is a new theorem prover.  It is a software system that is being developed at Microsoft and Carnegie-Mellon that allows mathematicians to verify proofs by computer.  This talk will give a general introduction to Lean for beginners.   (I am a beginner myself.) I will talk about installing the software, and writing simple proof scripts in the Lean theorem prover.