This repository contains the Lean code for the lecture notes The mechanics of proof, by Heather Macbeth, developed for the course Math 2001 at Fordham University.

The Lean files corresponding to each chapter of the lecture notes are in the folder Math2001.

You can run the code on the web using Gitpod, by clicking this link:

(You will be prompted to make an account, if you do not yet have one -- the free tier offers 50 hours of use per month.) This is the easiest way to get started if you have never used Lean before. You can accept the default "New Workspace" options and hit the "continue" button, then it will take about 90 seconds to load up a new workspace and auto-install the Lean mathematical library (wait for all the "cloning", "building", "downloading" and "decompressing" steps to finish). The workspace you just created will be accessible later from your Gitpod user page.

You can also install Lean to your own computer, then clone this repository to your computer by typing git clone https://github.com/hrmacbeth/math2001.git at the command line. This will let you run the code on your computer.