Formalizing Mathematics in LEAN

Here is a collection of things that you can look into to find a project topic. Of course this is not exhaustive, please come to us with your own project ideas on any topic in math/cs.

Here is an extensive list of topics, many of them with links to background info, on undergrad mathematics topics that are not yet in mathlib.

Here is the Github for mathlib, specifically the issues that are flag as beginner friendly to formalize.

Take a look at CSlib, the formalizing effort for computer science. There are still many topics on which you can work.

If you are interested in Physics, you might be interested in the PhysLean project that aims to formalize proofs in many areas of physics. There is an extensive list of varying degree theorems and statements that want to be formalized.

Something else worth formalizing is problems and solutions of the Putnam competition, a university level math test. There are already existing efforts to formalize these problems, but they are far from complete.

Take a look at "Proofs from THE BOOK" (Aigner, Ziegler. "Buch der Beweise"). There are tons of nice theorems and proofs in there, in beautiful form. While most of them have been formalized and/or exist in mathlib, you might still find some that are not or elegant proofs interesting enough for a project.