A Construction of the Lie Algebra of a Lie Group in Isabelle/HOL

TL;DR

This paper formalizes the theory of Lie groups and their Lie algebras in Isabelle/HOL, enhancing the formalization of differential geometry and continuous symmetries with correctness guarantees.

Contribution

It introduces a formal construction of the Lie algebra of a Lie group within Isabelle/HOL, addressing challenges in representing smooth structures in simple type theory.

Findings

Formalization of Lie groups and Lie algebras in Isabelle/HOL

Addresses integration of smoothness with simple type theory

Provides a foundation for advanced mathematical formalizations

Abstract

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.