Formalizing Geometric Algebra in Lean
cam.issuedOnline | 2022-04-18 | |
dc.contributor.author | Wieser, Eric | |
dc.contributor.author | Song, U | |
dc.contributor.orcid | Wieser, Eric [0000-0003-0412-4978] | |
dc.contributor.orcid | Song, U [0000-0003-3994-4466] | |
dc.date.accessioned | 2022-04-19T13:17:40Z | |
dc.date.available | 2022-04-19T13:17:40Z | |
dc.date.issued | 2022-07 | |
dc.date.submitted | 2021-03-17 | |
dc.date.updated | 2022-04-19T13:17:39Z | |
dc.description | Funder: Cambridge Commonwealth, European and International Trust; doi: http://dx.doi.org/10.13039/501100003343 | |
dc.description.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 $\mathbb{N}$-grading, and some of the gaps in mathlib that currently make this challenging. | |
dc.identifier.doi | 10.17863/CAM.83594 | |
dc.identifier.eissn | 1661-4909 | |
dc.identifier.issn | 0188-7009 | |
dc.identifier.other | s00006-021-01164-1 | |
dc.identifier.other | 1164 | |
dc.identifier.uri | https://www.repository.cam.ac.uk/handle/1810/336169 | |
dc.language | en | |
dc.publisher | Springer Science and Business Media LLC | |
dc.subject | Article | |
dc.subject | T.C. ICCA 12, Hefei, August 3-7, 2020 | |
dc.subject | Geometric Algebra | |
dc.subject | Clifford Algebra | |
dc.subject | Universal property | |
dc.subject | Lean | |
dc.subject | mathlib | |
dc.subject | Primary 15A66 | |
dc.subject | Secondary 68V20 | |
dc.title | Formalizing Geometric Algebra in Lean | |
dc.type | Article | |
dcterms.dateAccepted | 2021-07-22 | |
prism.issueIdentifier | 3 | |
prism.publicationName | Advances in Applied Clifford Algebras | |
prism.volume | 32 | |
rioxxterms.licenseref.uri | http://creativecommons.org/licenses/by/4.0/ | |
rioxxterms.version | VoR | |
rioxxterms.versionofrecord | 10.1007/s00006-021-01164-1 |
Files
Original bundle
1 - 2 of 2
Loading...
- 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/