10 minute Lean tutorial : proving logical propositions
Channel: Xena Project
Date: 2020-04-12

I show how to prove a basic result in logic using the Lean prover, first in tactic mode and then in term mode.

Try Lean online with no installation required at https://leanprover-community.github.io/lean-web-editor/

Instructions for installing Lean: https://github.com/leanprover-community/mathlib#installation