The Secret Agent and the Umbrella

This repository is part of the Imperial undergraduate workshop in Lean, taking place Sep 26 -- 30, 2022.

Installing Lean

• If necessary follow these steps to install Lean.
• Follow these steps to get started working on this project.

Try it out without installing

If you want to try things out without installing Lean then you can try using Gitpod.

Learning the mathematics

Read this document by Jiří Matoušek to learn about the Shannon capacity of a graph and to see how we can calculate this for the 5-cycle using a brilliant technique due to László Lovász.

Remember

We are here to ask questions, to learn some Lean, possibly to learn some mathematics, but also to meet each other and to have fun.