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

computer algebraClifford algebrageometric algebraautomatic proofsmathlibcomputer logic

Mathematics Subject Classification ID

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

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 $mathbbN$-grading, and some of the gaps in mathlib that currently make this challenging.

Recommendations

• Formalization of geometric algebra in HOL Light
• Implementing geometric algebra products with binary trees
• Formalization of geometric algebra theories in higher-order logic
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• scientific article; zbMATH DE number 1303337

Cites work

• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• Clifford algebra to geometric calculus. A unified language for mathematics and physics
• Clifford and Graßmann Hopf algebras via the BIGEBRA package for Maple
• Formalization of geometric algebra in HOL Light
• Garamon: a geometric algebra library generator
• Implementing geometric algebra products with binary trees
• Maintaining a library of formal mathematics
• Solving some quadratic Diophantine equations with Clifford algebra
• The Lean theorem prover (system description)

Cited in

(9)

• Graded rings in Lean's dependent type theory
• Schemes in Lean
• Exploring formalisation. A primer in human-readable mathematics in Lean 3 with examples from simplicial topology
• A formalization of Grassmann-Cayley algebra in Coq and its application to theorem proving in projective geometry
• Formalising the Kruskal-Katona theorem in Lean
• Survey of new applications of geometric algebra
• Formalization of geometric algebra theories in higher-order logic
• Formalizing double groupoids and cross modules in the Lean theorem prover
• Computing with the universal properties of the Clifford algebra and the even subalgebra

Describes a project that uses

Uses Software

• mathlib
• Garamon
• Archive Formal Proofs
• MathOverflow
• Lean
• GAlgebra
• Agda
• Sledgehammer
• HOL Light
• Mathematica
• Coq
• CLIFFORD
• BIGEBRA

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)