<p>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 useful in the study of continuous transformations in fields such as particle physics and robotics. The formalisation of this theory in an interactive theorem prover poses challenges beyond those encountered in textbook developments. We comment on representational choices we made to integrate involved concepts, such as smoothness of vector fields, with the simple type theory of higher-order logic (HOL) and existing material in Isabelle/HOL.</p>