Skip to content

Lean material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics.

Notifications You must be signed in to change notification settings

nivasan1/formalising-mathematics-2022

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Formalising Mathematics

This is the repository for Kevin Buzzard's 2022 course on formalising mathmatics in the Lean theorem prover. The course ran from January to March 2022. Note: the 2023 version of the course is here.

Installation

If you have Lean 3 and the community tools installed, then it's just a matter of typing

leanproject get ImperialCollegeLondon/formalising-mathematics-2022

into the command line. Instructions for installing Lean 3 and the relevant tools are here.

Course notes

The course notes are here. Note: the 2023 course notes are more up to date.

Course videos

The accompanying videos are in a YouTube playlist here.

About

Lean material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 100.0%