Formalizing Geometric Algebra in Lean

TL;DR

This paper formalizes Geometric (Clifford) algebras within the Lean 3 theorem prover, introducing a basis-independent approach and demonstrating how to define key algebraic operations using the universal property.

Contribution

It presents a novel basis-independent formalization of Clifford algebras in Lean, leveraging the universal property and addressing gaps in mathlib.

Findings

Formalization of multivectors as tensor algebra quotients

Establishment of the universal property of Clifford algebra

Definition of involutions, versors, and grading using the universal property

Abstract

This paper explores formalizing Geometric (or Clifford) algebras into the Lean 3 theorem prover, building upon the substantial body of work that is the Lean mathematics library, mathlib. As we use Lean source code to demonstrate many of our ideas, we include a brief introduction to the Lean language targeted at a reader with no prior experience with Lean or theorem provers in general. We formalize the multivectors as the quotient of the tensor algebra by a suitable relation, which provides the ring structure automatically, then go on to establish the universal property of the Clifford algebra. We show that this is quite different to the approach taken by existing formalizations of Geometric algebra in other theorem provers; most notably, our approach does not require a choice of basis. We go on to show how operations and structure such as involutions, versors, and the $\mathbb{Z}_2$-grading can be defined using the universal property alone, and how to recover an induction principle from the universal property suitable for proving statements about these definitions. We outline the steps needed to formalize the wedge product and $\mathbb{N}$-grading, and some of the gaps in mathlib that currently make this challenging.