Lean is a theorem prover and programming language based based on the calculus of constructions with inductive types. This repo is for my own exploration of Lean and Mathlib.
- Lean Language
- Formal mathematical argumentation
- Completed all tutorials in this repository.
- Completed the natural number game (https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/)