Formalizing Hall's Marriage Theorem in Lean. - Alena Gusakov; Bhavik Mehta; Kyle A. Miller (CoRR, 2021)

Formalising Szemerédi's Regularity Lemma in Lean. - Yaël Dillies; Bhavik Mehta (ITP, 2022)

Formalising the Kruskal-Katona Theorem in Lean. - Bhavik Mehta (CICM, 2022)

Formalising Sharkovsky's Theorem (Proof Pearl). - Bhavik Mehta (CPP, 2023)