  Lie algebras are an important class of algebras which arise throughout
mathematics and physics. We report on the formalisation of Lie algebras in
Lean's Mathlib library. Although basic knowledge of Lie theory will benefit the
reader, none is assumed; the intention is that the overall themes will be
accessible even to readers unfamiliar with Lie theory.
  Particular attention is paid to the construction of the classical and
exceptional Lie algebras. Thanks to these constructions, it is possible to
state the classification theorem for finite-dimensional semisimple Lie algebras
over an algebraically closed field of characteristic zero.
  In addition to the focus on Lie theory, we also aim to highlight the unity of
Mathlib. To this end, we include examples of achievements made possible only by
leaning on several branches of the library simultaneously.
