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

This article is part of the Topical Collection on Proceedings TC ICCA 12, Hefei, 2020, edited by Guangbin Ren, Uwe Kähler, Rafał Abłamowicz, Fabrizio Colombo, Pierre Dechant, Jacques Helmstetter, G. Stacey Staples, Wei Wang.

Geometric Algebra provides a language for manipulating geometry algebraically, which unifies many geometric applications of complex numbers, quaternions, and linear algebra into a single mathematical language.

There are software packages in various languages today which support working with and developing intuition for Geometric Algebra. Most of these packages are designed for numerical computation, typically targeted somewhere along the spectrum with ease of use at one end and efficiency at the other. However, it is the packages designed for symbolic manipulation which are most relevant to the topic of this paper, such as the packages for Python [

A key feature in a CAS is the ability to simplify expressions to save the user from doing so manually, which can be slow and error-prone. Such a system is preloaded with a set of rules, such as

Theorem provers take quite a different approach—the base set of axioms is very small (for example, those of Zermelo–Fraenkel set theory), and every other “rewrite rule” must be proven from these. This approach drastically reduces the amount of trust needed from the user—instead of having to place trust in every single rewrite rule, their trust can be concentrated onto: the theorem prover itself, its choice of axioms, and the fact that the definitions used in the rewrite rule correspond to their established meaning

One such theorem prover is Lean [

This paper will start in Sect.

Geometric algebra (GA)

A geometric algebra is characterized by its metric, a quadratic form

A key advantage to using GA for geometric problems is that it is rarely necessary to explicitly separate coordinates when doing geometry, as would be done for instance when constructing a rotation matrix or computing the intersection of two planes. In a numerical software package, internally representing coordinates is unavoidable; but for symbolic manipulation, coordinates can just be a distraction. For this reason, we would prefer a formalization that avoids coordinates entirely.

Theorem proving software must do more than simply encode and verify mathematical truth; it must make doing so ergonomic for the user, and minimize the inevitable friction when converting a pen and paper argument into a machine-readable one. The typical workflow for this conversion is split into two parts—translating the theorem statement, and then translating the proof.

The use of dependent type theory (as opposed to the set theory typically used by mathematicians) helps with the theorem statements, as it provides a mechanism to reject nonsensical statements like

Where the software can really shine though is in the proofs, via interactive and automated theorem proving. The former is about showing unresolved “goals” as the proof progresses, to help the user as they write and to guide them what to do next. The latter is invaluable for discharging goals the user views as trivial, such as

The Lean 3 language used in this paper is just one of many theorem proving languages, and while it has all of the properties described above, it is not unique in that it does so. Its use of dependent types is very similar to Coq, and its heavy use of notation similar to Agda. Its automation tools are currently less powerful than those of Isabelle/HOL, without an equivalent to Isabelle/HOL’s powerful

In this section, we will give a very brief introduction to the Lean language, in order to aid with reading the fragments of Lean code

We’ll start with a simple definition, showing how to define a value with a given name and type. Here, we define the name

Usually we do not separate our statements and proof as we did for

The second line of this proof enters

The logical foundation of Lean is the Calculus of Inductive Constructions. The following example demonstrates a typical inductive construction; an inductive type used to represent the logical or of two propositions:

This reads as “there are two ways to construct a proof of

These “inductive” types are used to build almost every object needed in formalized mathematics and computer science; examples include the integers, lists, logic operators, and existential quantifiers. Sometimes we need one more fundamental building block, “quotient” types. These allow associating an equivalence relation with a type, for instance to ensure that

By itself, Lean is very much “batteries not included”. Its standard library is not opinionated on whether you use it for mathematics or software verification, and as a result comes with little beyond basic data types

The mathematically interesting statements come from mathlib, which is “a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant” [

The coherency and breadth of this library makes formalization work in Lean particularly attractive, as new structures can often be built as a thin layer on top of existing structures. Furthermore, it reduces the effort needed to bring formalizations in different branches of mathematics together—for instance, in the process of formalizing statements about the wedge product in this work (Sect.

Lean is not unique in having a standard library of mathematics—two obvious contenders are the math-comp of Coq, and the stdlib of Agda. A thorough comparison of the three libraries is beyond the scope of this paper, but a very rough estimate of breadth and accessibility to new users can be obtained by counting the lines of code, comments, and contributors, as shown in Table

Comparison of metrics between standard libraries of popular provers using data from their GitHub repositories as of July 2021

Language | Library | Source lines | Comment lines | Contributors |
---|---|---|---|---|

Lean | mathlib | 388k | 100k | 159 |

Agda | agda-stdlib | 66.9k | 20.4k | 98 |

Coq | math-comp | 95.9k | 7.6k | 35 |

Hol-light | 707k | 40.4k | 8 | |

Isabelle | AFP | 4.26M | 108k | 386 |

^{1} Counted using the scc program.

^{2} According to git. Some projects do not record all authors here.

^{3} The standard library and language are hard to distinguish, so the metrics include both.

^{4} The “Archive of Formal Proofs” is not a standard library but a collection of libraries, and as such is larger but less interlinked.

Our intent in formalizing Geometric Algebra is for our formalization to not only interface well with mathlib, but also for certain portions to ultimately end up a part of it. Contributing code into mathlib ensures its ongoing maintenance [

In the rest of this section, we will introduce the elementary parts of mathlib that will be essential to both translating existing formalizations and constructing our own.

Some of the simplest definitions provided by mathlib are those of the algebraic structure hierarchy—statements like “the type

Of particular interest to formalization of geometric algebra are

In mathematics, it is frequently useful to talk about structure-preserving morphisms, such as an

Notation for homomorphisms in mathlib

While there has been no published use of Lean to formalize geometric, Clifford, or Grassman–Cayley algebras, there are already formalizations in other theorem proving languages. To aid the reader, when describing these other formalizations this section presents code snippets translated into their (roughly) equivalent Lean code.

Of particular interest in these existing formalizations is the underlying definition used to define a multivector, and how this definition can be used to define a product of some kind. While proofs are obviously important to a formalization, every proof has to start with a theorem statement, the expressivity of which is limited by the definitions at hand.

We present them roughly in order of generality.

In [

The problem only becomes worse when defining the geometric product, as now we have four terms in each of the components. As in [

The tedium of the component-wise definitions and proofs can be reduced by generation from CAS implementations and automation features within the theorem provers, but this scales poorly to more complex statements, which may need to be tackled by hand. Needless to say, this formalization does not scale at all to other dimensions and signature of algebra, as no part of it is generalized.

A convenient way to escape this death-by-cases is to use a recursive definition of a multivector. This is the approach taken by the Coq formalization of Grassmann–Cayley algebra in [

The recursive data definition leads naturally to a recursive operator definition, which resembles the following:

While [

The HOL light formalization in [

Overall, the formalization that follows in [

To mesh well with mathlib, our formalization will need to support algebras over a variety of vector spaces, not just those with coefficients in

In this section, we present a variety of definitions and theorems for GA that we formalized in Lean. For reasons described in Sect.

While it is typical on paper to avoid distinguishing “the multivectors of grade zero” from “the scalars”, or “the multivectors of grade 1” from “the vectors”, the strict dependent typing of Lean forces us to treat these separately. Instead of saying that the multivectors

Typically we would assume these mappings are injective, but we can obtain many results without needing to do so. As it turns out, the definitions outlined below permit these maps to be non-injective, for particularly pernicious choices of

A Clifford algebra over the vector space

As of writing, mathlib does not have direct support for two-sided ideals, but it does support the equivalent operation of taking the quotient by a suitable closure of a relation like

The operations described in Sect.

The remaining code to explain is our

While not written by the authors, a better understanding of the power of inductive types can be obtained by looking inside mathlib’s definition of

While convenient to define, the quotient can be hard to state further definitions and prove theorems about. When defining operations over a quotient, the approach is almost always to operate on the data within the quotient, and then prove that for any operands that are considered equal under the quotient, the output of the operation is unchanged.

Such proofs can be very challenging, especially given some short-comings in Lean when it comes to recursing over nested inductive types (such as

The universal property can be stated in Lean as

Note that if we apply this equivalence in reverse to the identity algebra automorphism

The type of

For the rest of our formalization, our proofs and definitions depend only on the properties of

Beyond the identity mapping

A similar approach can be performed to define grade reversion

While the above definitions of

The induction principle we seek can be stated “If a property

Show that collectively, the inputs to our inductive principle define a

Restrict the codomain of

Lift this restricted map from

Apply this lifted map to our input

An algebra

Instead, we can show that the Clifford algebra permits a

To finish this definition of the grading, we show that there is

The versors can be described as a set of multivectors closed under multiplication

Lean provides some useful syntax for working with sub-objects like this. Instead of working with

Armed with our definition, the next step is to once again construct an induction principle. Most of the heavy lifting is done by the

The induction principle lets us once again bash out some useful statements with uninteresting proofs. This time, we scratch the surface of Lean’s meta-programming framework to avoid repeating a trivial proof:

Formalizing the wedge product of

Of course, a crucial use of the wedge product is between arbitrary multivectors, not just basis vectors. The ideal way to define this wedge product would be to find a linear isomorphism

Our work does not go as far as defining the

One way to do so would be to first show that the Clifford algebra is a filtered algebra, in that it can be split into subsets

The definition of a filtered algebra, along with a proof that a Clifford algebra satisfies it with

Interestingly, it can be shown that such an isomorphism does not always exist; as mentioned in Sect.

In Sect.

For a more illustrative example than the complex numbers, we will use the rest of this section to outline how to set up a definition of Conformal Geometric Algebra,

We start by defining the conformalized vector space of a real vector space as the triple of (original vector space

With our definitions out of the way, our next job is to train the Lean simplifier about trivial combinations of these functions

A construction of PGA in Lean can be done in very much the same way, and is included in our source repository.

In Sect.

To date, mathlib does not have a reusable definition for graded modules and algebras, making it difficult to make definitions that can be reused across tensor, exterior, and Clifford algebras. In Sect.

A better solution would be to use mathlib’s

As mentioned in Sect.

Parallel to our efforts to formalize geometric algebra, mathlib has been making great progress in the field of analysis, with slowly improving support for multivariate calculus. A notable result in the last few months was the formalization of variations of the Fundamental Theorem of Calculus.

As this part of mathlib matures, it should be possible to formalize the Geometric Calculus described by [

We have shown how Lean can be used to formalize Geometric Algebra in a variety of ways. Of these ways, we chose to develop the formalization using a quotient definition, as this offered greater generality than any previous formalization. We demonstrate how to use the universal property of the Clifford algebra that this definition provides to recover additional definitions and operators, and how to prove that these constructions behave as we intend. To demonstrate the generality of our approach, we show how to specialize it to a Conformal Geometric Algebra over a vector space of arbitrary dimension. Throughout, we make liberal use of the mathlib library for Lean, demonstrating the convenience of having an expansive body of formalized mathematical terminology stated coherently in a single place.

A complete archive consisting of our formalization, our translations of parts of existing formalizations, the precise versions of Lean and mathlib that our code is compatible with, and a summary of the various contributions to mathlib made as part of this work can be found on GitHub at

mathlib is not only growing quickly, but changes quickly too. Through having contributed the key definitions from our work back into mathlib, we ensured these definitions will change with it, and can be built upon in future by others.

We would like to thank the mathlib community for their valuable and rapid support for all questions about Lean and mathlib. The first author is supported by a scholarship from the Cambridge Trust.

e.g., A rule can state

Often used interchangeably with Clifford algebra.

Although not assumed throughout this paper.

Note that Lean source code makes heavy use of non-ASCII unicode characters, which some PDF readers are unable to copy to the clipboard faithfully. Unfortunately, Lean source code cannot be copied at all from the web version of this paper.

Which may in future run a version of Lean incompatible with the code samples in this paper. A compatible version can be ensured by using the configuration in our GitHub repository in Sect.

Here and in Lean,

Which themselves require

The

The names of which are taken from mathlib conventions.

A partial formalization of this result was shown in Lean.

But thankfully, also proven by Lean!

Which corresponds to requiring that the submodules

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.