Formalizing geometric algebra in Lean (Q2128117)

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''.