Formalizing Geometric Algebra in Lean. - Eric Wieser; Utensil Song (CoRR, 2021)