Formalizing Clifford algebras and related constructions in the Lean theorem prover

Geometric Algebra (GA) is a mathematical framework used primarily by engineers and physicists, while theorem proving software has its background originally in computer science departments. This thesis brings the former into the language of the latter, in the more abstract setting of Clifford algebras. It does so via the theorem proving language “Lean”, which is seeing increasing adoption in mathematics departments. The focus is much broader than simply formalizing Clifford algebras; Lean has an expansive and monolithic library of formalized mathematics, mathlib, which the author made Clifford algebras a part of. Over the course of this work, mathlib was reshaped and extended in various ways. Part I of this thesis provides an introduction to geometric algebra, Clifford algebra, and an exploration of the author’s path from numerical software through symbolic tools to the Lean theorem prover. Part II describes the various ways in which mathlib’s algebra libraries were shaped by the author, covering: the use of typeclasses to manage automatic inference of scalar actions, the use of the extensionality “tactic” to provide leverage when proving results about complicated algebraic objects, a novel formalization of graded monoids, rings and algebras, and a deeper dive into intricate traps around typeclasses that originate in the language itself. Part III begins by illuminating informally how to build a library of results around Clifford algebras using the universal property alone, then uses this approach to constructively build an expansive set of well-known isomorphisms in a basis-free manner; contributing many formalizations relating to other algebraic topics to mathlib along the way. These topics include dual quaternions, tensor products, quadratic forms, alternating maps, and exponential operators. As well as summarizing the author’s key contributions and possible avenues for future development, the conclusions outline how other users of Lean are already building upon parts of the author’s work.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2024

Author dc:creator

• Wieser, Eric

Advisor dc:contributor.advisor

• Lasenby, Joan

• clifford algebras
• formal mathematics
• geometric algebra
• interactive theorem proving
• Lean prover

Licence

• https://apollo8-f-pro.lib.cam.ac.uk/bitstreams/a8121834-5983-431e-b863-f186fce1d184/download
• https://creativecommons.org/licenses/by/4.0/

Language dc:language

eng

Author Identifier

0000-0003-0412-4978

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/370602