This is the repository for the module MA4N1 Theorem Proving with Lean at the University of Warwick.
Here, you will find the Lean files used during lectures, some exercises and various complements.
This is a Lean project with Mathlib
as a dependency.
You may want to set-up something like this for your group project.
You can find instructions on how to do this at this webpage.
For systems other than Unix, take a look at the Mathlib projects webpage.