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.
翻译:本文探索将几何值( 或克里夫多德) 代数正规化为利昂 3 理论证明, 以利昂数学图书馆( Mathlib ) 的大量工作为基础。 我们使用利昂源代码来展示我们的许多想法, 我们用利昂源代码来简要介绍利昂语言, 特别是针对一个在利昂或理论证明者方面没有经验的读者。 我们通过一种合适的关系, 将多元代数的商数( 或克里夫代数) 正式化为高温代数的商数, 自动提供环形结构, 然后继续建立克利福德代数的通用属性。 我们表明这与在其它理论验证中现有的地基代数代数正规化方法非常不同; 最明显的是, 我们的方法并不需要选择基础。 我们继续展示如何使用通用属性来界定多维值的操作和结构, 以及 $mathbb2 =2 递增值, 如何从通用属性中恢复一项上位原则, 以适合证明这些定义的通用值。 我们勾勒格 和数学需要的步骤来正式化。