A∞-categories in Lean Marco David, Jason Dong, Hallvard Hareide, Jasper van de Kreeke, Justin Mu, Niels Voss, Annie Yao Repository for the URAP formalization project at UC Berkeley.