Abstract by Jeremy Avigad:

We will describe some of the features and design goals of a new, open source, interactive theorem proving system called Lean. Many of Lean's features are specifically designed to support homotopy type theory, and provide a solid foundation for carrying out formal developments in HoTT. Lean's HoTT library already includes most of the theorems in the HoTT book, support for cubical reasoning, and category theory. We will provide an overview of the library, and discuss current and ongoing work in synthetic homotopy theory.

Abstract by Floris van Doorn:

Lean is a new proof assistant which is designed to support Homotopy Type Theory. Lean has a built-in HoTT library, which contains a solid foundation for doing HoTT, including almost all theorems in Chapters 1-7 of the HoTT-book. In addition, the library contains category theory and various theorems in synthetic homotopy theory.