MTH1001 Tutorial

A Lean introduction to pure mathematics.

These sheets are (currently) a tutorial introduction to:

• Propositional Logic
• Predicate Logic
• Natural numbers and induction
• Sets
• Functions
• Real numbers

Installation

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/mth1001_tutorial.

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.

About the project

Designed by Gihan Marasingha for the undergraduate module MTH1001 (Mathematical Structures) at the University of Exeter.