search

hrmacbeth / math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant
152 stars 59 forks source link
lean4

readme

The Mechanics of Proof

This repository contains the Lean code for the book 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 book are in the folder Math2001.

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

Open in Gitpod

(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 five minutes to load up a new workspace and auto-install the Lean mathematical library (wait for all the "cloning", "building", "compiling", "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.