formalising-mathematics

Tech stack & purpose

This repository contains Lean 3 material for an EPSRC Taught Course Centre course on formalising mathematics delivered by Kevin Buzzard at Imperial College London in January–March 2021 to mathematicians at Imperial, Oxford, Bristol, Bath, and Warwick. The course teaches mathematical theorem proving by formulating mathematics problems as interactive puzzle games in Lean, progressing from basic logic and set theory through group theory, topology, filters, limits, quotients, and group cohomology across eight workshops. The material is built in Lean 3 (now end-of-life) and includes instructions for installation via the leanproject tool, with alternatives for working in the community web editor, along with detailed documentation of Lean tactics needed to solve the puzzles.

Community & reference links

• leanprover-community.github.io
• logic
• sets
• functions
• relations
• click here to play Part A online
• Lean Zulip chat
• Introduction
• Logic, sets, functions, relations
• Groups and subgroups
• Sequences and limits
• Topology
• Filters
• Limits
• Quotients
• Group cohomology
• natural number game

Languages

Contributors

• 
  Kevin Buzzard201 commits · 946 followers