A project for investigating the real number system via the interactive theorem prover Lean.
To use this project, ensure you have installed Lean and Visual Studio Code via the instructions at the Lean Prover Community.
Open a terminal window in VSCode and type
leanproject get https://github.com/gihanmarasingha/ems_reals.
This will download the project into the current folder on your computer. Open this folder in
VSCode and start working on the exercises contained in the src/exercises folder.
Designed for the Exter Mathematics School by Gihan Marasingha based on his materials for the undergraduate module MTH1001 (Mathematical Structures) at the University of Exeter.