Welcome!
This blog will discuss the topics we cover as we learn th every basics of the Lean proof assistant:
- https://en.wikipedia.org/wiki/Lean_(proof_assistant)
- https://leanprover-community.github.io
- https://lean-lang.org
Audience & Scope
The reason this blog exists is to address the fact that a proof assistant is really cool, but almost all the tutorials and guides are too difficult for those of us who are not already familiar with proof assistant and advanced mathematics - and the high barrier of jargon that goes with it.
The aim is to gain enough understanding of Lean to be able to prove simple theorems, and to give us the grounding and confidence to learn more if we wish to.
Proof Assistant?
It is worth clarifying what Lean is and isn't. It isn't a magic tool for coming up with proofs.
It is a proof verifier, which means we provide proofs and Lean checks to see if they are valid.
