Getting started with the Lean theorem prover

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.