  This paper describes a formal theory of smooth vector fields, Lie groups and
the Lie algebra of a Lie group in the theorem prover Isabelle. Lie groups are
abstract structures that are composable, invertible and differentiable. They
are pervasive as models of continuous transformations and symmetries in areas
from theoretical particle physics, where they underpin gauge theories such as
the Standard Model, to the study of differential equations and robotics.
Formalisation of mathematics in an interactive theorem prover, such as
Isabelle, provides strong correctness guarantees by expressing definitions and
theorems in a logic that can be checked by a computer. Many libraries of
formalised mathematics lack significant development of textbook material beyond
undergraduate level, and this contribution to mathematics in Isabelle aims to
reduce that gap, particularly in differential geometry. We comment on
representational choices and challenges faced when integrating complex
formalisations, such as smoothness of vector fields, with the restrictions of
the simple type theory of HOL. This contribution paves the way for extensions
both in advanced mathematics, and in formalisations in natural science.
