This is the repository is a fork of Kevin Buzzard's 2022 course on formalising mathmatics in the Lean theorem prover.
I added a applied_math and contest math folder.
The goal is to formalize the basic lemmas and tactics (meta programs) necessary to prove problems typically found in a highschool level math competitions.
You can open my workspace in the browser using gitpod: https://gitpod.io/#https://github.com/FrederickPu/formalising-mathematics-2022