I have been involved in the supervision of several undergraduate Lean projects since 2017. Here are some examples.
Kenny Lau — formalisation of the statements of the local Langlands conjectures for abelian algebraic groups. First year undergraduate project 2018. Won the pure project prize. GitHub. Kenny formalised a lot of the structures necessary to state the local Langlands correspondence for tori.
Chris Hughes — formalisation of proofs of Sylow’s Theorems. First year undergraduate project 2018. Github. Chris proved all of Sylow’s theorems in Lean, and his proof of Sylow 1 is now in mathlib.
Ali Sever — Euclidean geomety in Lean. Summer project 2018. GitHub. Ali formalises Tarski’s version of Euclidean geometry.
Ramon F. Mir — Schemes in Lean. MEnd project 2019. Won the JMC maths project prize. Github. Ramon gave a definition of schemes in Lean; his ideas were incorporated in mathlib recently.
Anca Ciobanu — Group Cohomology in Lean. BEng project 2019. pdf and GitHub. Anca defined H^0 and H^1, and proved the long exact sequence of terms of low degree in group cohomology.
Lambert A’Campo and Ashvni Narayanan — compact unit ball implies finite-dimensional. LSGNT computing project 2019. GitHub. Lambert and Ashvni prove that if a normed vector space over a nondiscrete complete normed field has compact unit ball then it is finite-dimensional.
Shenyang Wu — Group Cohomology in Lean. MSci project 2020. GitHub. Shenyang defined H^n for all n. Here is his write-up.
Ellen Art — Dots and boxes in Lean. MSci project 2020. GitHub. Ellen develops the theory of the man in the middle in Lean.
Xiang Li — Eudoxus’ construction of the reals. Xena summer project 2020. Github. Xiang develops the theory of reals as equivalence classes of “almost linear” functions from the integers to itself.
Harun Khan — Squares in the Fibonacci sequence. Xena summer project 2020. Github. Harun formalised Cohn’s proof that 144 is the largest square in the Fibonacci sequence.
Jamie Bell — a statement of the Birch and Swinnerton-Dyer conjecture. LSGNT student mini-project 2021. Github. Jamie formalised a statement of the BSD conjecture. He did not prove all intermediate results along the way (for example he did not prove that the L-function of an elliptic curve has a holomorphic extension to a neighbourhood of 
Other projects
The Leanprover-community website also has a list of projects which use Lean or mathlib.
Xena 