Formalising perfectoid spaces. - Kevin Buzzard; Johan Commelin; Patrick Massot (CPP, 2020)

Formalising the h-Principle and Sphere Eversion. - Floris van Doorn; Patrick Massot; Oliver Nash (CPP, 2023)

Teaching Mathematics Using Lean and Controlled Natural Language. - Patrick Massot (ITP, 2024)