eigenblade.ninja
I came to geometric algebra from computer graphics, and stayed for the proofs.
I build implementations of conformal geometric algebra for robotics in five languages, and check them against one another, including a Lean 4 formalization tied to Mathlib. Along the way I have been making the case that the outer product carries the wrong sign.
Essay
Geometric algebra writes the product that joins subspaces with ∧, the sign the rest of mathematics uses for meet. This essay argues the case in two manners, after Hermann Grassmann and after David Hestenes, and proposes transitional glyphs that carry the old sign inside the new.
Read the essay →Conformal geometric algebra, CGA(4,1), for robot kinematics, implemented in C++, Rust, Julia, Idris 2 and Lean 4. The implementations are cross-checked against shared fixtures; when a silent sign-convention split between them surfaced, it was resolved family-wide by a declared decision.
A Lean 4 formalization of CGA(4,1) whose laws are kernel-checked theorems. It proves the concrete multiplication table equal to Mathlib's abstract CliffordAlgebra, so associativity is inherited rather than re-checked.
A LaTeX package for the transitional wedge and antiwedge symbols, drawn in TikZ, which typeset as drop-in replacements for \wedge and \vee.