MA4N1 Theorem Proving with Lean

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.

Back to the Theorem Proving with Lean webpage

Back to Moodle

Open in Gitpod