Formalizing geometric algebra in Lean

DOI10.1007/S00006-021-01164-1MaRDI QIDQ2128117zbMATH OpenOpenAlexWikidataFDO

Authors Eric Wieser, Utensil Song

Publication date 21 April 2022

Published in Advances in Applied Clifford Algebras (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2110.03551

zbMATH Keywords

automatic proofs Clifford algebra computer algebra computer logic geometric algebra mathlib

Mathematics Subject Classification ID

Quadratic spaces; Clifford algebras (11E88) Clifford algebras, spinors (15A66) Applications of Clifford algebras to physics, etc. (15A67) Formalization of mathematics in connection with theorem provers (68V20)

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

m a t h b b 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

m a t h b b N

-grading, and some of the gaps in mathlib that currently make this challenging.

Review text

The paper is written for graduate students and researchers in the field of mathematics, computer science, and in particular Clifford geometric algebras and their applications. It outlines the first steps towards the formalization of geometric algebra for the Microsoft Research Lean system, in particular to work with its mathematics library ``mathlib. Such a library is used by a wide community with over 100 contributors, and in the paper it is compared to Agda, Coq, Hol Light and Isabelle AFP (Archive of Formal Proofs). The authors describe their approach in detail (type theory, quotient definition, Clifford algebra universal property, conjugations, induction, \(\mathbb{Z}_2\)-grading, versors, wedge product, conformal geometric algebra), also giving a number of Lean code examples with comments. As for future work they emphasize the importance of working in Lean with graded modules and algebras, coordinate-free definition of the wedge product (Clifford algebra to exterior algebra isomorphisms), and the formalization of geometric calculus. All codes created by the authors are open source and available in a GitHub repository, and a part of their codes has already been integrated into Lean's ``mathlib.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

This page was built for publication: Formalizing geometric algebra in Lean

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2128117)