Formalising Mathematics

This is the repository is a fork of Kevin Buzzard's 2022 course on formalising mathmatics in the Lean theorem prover.

My Contributions

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.

Try it out!

You can open my workspace in the browser using gitpod: https://gitpod.io/#https://github.com/FrederickPu/formalising-mathematics-2022