Skip to content

ImperialCollegeLondon/M1P1-lean

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

57 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

M1P1-lean

Material from M1P1, formalised in Lean

I am writing heavily-commented Lean proofs of results from Imperial's M1P1 course, and example sheet questions. The general aim is to turn the material into a fully formalised mathematics textbook covering basic 1st year analysis.

I will be giving talks about this repository on Tuesdays 1-2 in Huxley 140 during the Spring 2019 term.

Kevin Buzzard

Installation instructions

First you need to install Lean and and the mathlib helper scripts, by following the instructions here at the mathlib github repository.

Once you have these, you can install this project with the following incantations:

git clone [email protected]:ImperialCollegeLondon/M1P1-lean.git
cd M1P1-lean
leanpkg configure
update-mathlib

Then go to VS Code and use the File -> Open Folder option (this is important) and open the project folder.

About

Material from M1P1, formalised in Lean

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 3

  •  
  •  
  •  

Languages