Introduction
The goal of this document is to provide a detailed account of the formalization of Geometric Algebra (GA) a.k.a. Clifford Algebra [ Hestenes and Sobczyk(1984) ] in the Lean 4 theorem prover and programming language [ Moura and Ullrich(2021) , de Moura et al.(2015) , Ullrich(2023) ] and using its Mathematical Library Mathlib [ The mathlib Community(2020) ] .
The PDF version of this blueprint is available here.