Repository logo
 

Formalizing Geometric Algebra in Lean

cam.issuedOnline2022-04-18
dc.contributor.authorWieser, Eric
dc.contributor.authorSong, U
dc.contributor.orcidWieser, Eric [0000-0003-0412-4978]
dc.contributor.orcidSong, U [0000-0003-3994-4466]
dc.date.accessioned2022-04-19T13:17:40Z
dc.date.available2022-04-19T13:17:40Z
dc.date.issued2022-07
dc.date.submitted2021-03-17
dc.date.updated2022-04-19T13:17:39Z
dc.descriptionFunder: Cambridge Commonwealth, European and International Trust; doi: http://dx.doi.org/10.13039/501100003343
dc.description.abstractThis 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.
dc.identifier.doi10.17863/CAM.83594
dc.identifier.eissn1661-4909
dc.identifier.issn0188-7009
dc.identifier.others00006-021-01164-1
dc.identifier.other1164
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/336169
dc.languageen
dc.publisherSpringer Science and Business Media LLC
dc.subjectArticle
dc.subjectT.C. ICCA 12, Hefei, August 3-7, 2020
dc.subjectGeometric Algebra
dc.subjectClifford Algebra
dc.subjectUniversal property
dc.subjectLean
dc.subjectmathlib
dc.subjectPrimary 15A66
dc.subjectSecondary 68V20
dc.titleFormalizing Geometric Algebra in Lean
dc.typeArticle
dcterms.dateAccepted2021-07-22
prism.issueIdentifier3
prism.publicationNameAdvances in Applied Clifford Algebras
prism.volume32
rioxxterms.licenseref.urihttp://creativecommons.org/licenses/by/4.0/
rioxxterms.versionVoR
rioxxterms.versionofrecord10.1007/s00006-021-01164-1

Files

Original bundle
Now showing 1 - 2 of 2
Loading...
Thumbnail Image
Name:
6_2021_Article_1164.pdf
Size:
654.91 KB
Format:
Adobe Portable Document Format
Description:
Published version
Licence
http://creativecommons.org/licenses/by/4.0/
No Thumbnail Available
Name:
6_2021_Article_1164_nlm.xml
Size:
163.04 KB
Format:
Extensible Markup Language
Description:
Bibliographic metadata
Licence
http://creativecommons.org/licenses/by/4.0/