Stars
Lean 4 programming language and theorem prover
Lean 3's obsolete mathematical components library: please use mathlib4
Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.
A simple REPL for Lean 4, returning information about errors and sorries.
Source code for the Mathematics in Lean tutorial.
Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024
Some examples of Lean projects, for undergraduate mathematicians.
Some theorems presented to first and second year mathematics undergraduates, First and second year undergraduate level mathematics
Formalizing John H. Conway's 1986 FRACTRAN paper in Lean4
Formalizing the basic definitions and results of polyhedral geometry in Lean 4.