From Zero to QED: An informal introduction to formality with Lean 4
3 days ago
- #Lean 4
- #Functional Programming
- #Theorem Proving
- From Zero to QED is an informal introduction to Lean 4, aiming to fill gaps in scattered learning resources.
- The series is divided into two arcs: programming in Lean (syntax, type system, monads, IO) and theorem proving (proofs, tactics, dependent types).
- No prior theorem prover experience is needed; familiarity with typed functional languages like Haskell is helpful but not required.
- The project is backed by machine-verified code on GitHub, ensuring accuracy and reliability.
- Lean 4 installation and repository cloning instructions are provided for local setup.
- Additional formal resources are listed for those seeking rigorous introductions to Lean 4 and theorem proving.