A Leibniz algebra is a nonassociative algebra that satisfies the (right) Leibniz identity: (ab)c = (ac)b + a(bc). In other words, right-multiplication by any element acts as a derivation of the algebra. This is more general than a Lie algebra, since the product need not be skew-symmetric. (The product is often written as a bracket [a,b], but I will stick with ab for now.) Since we don't require our algebra to be associative or commutative, there are many ways to arrange n given elements into a product. For example, with four elements a,b,c,d we have a(b(cd)), a((bc)d), (ab)(cd), ((ab)c)d, (a(bc))d plus the other products that one gets from permuting the symbols a,b,c,d. One cool thing is that in a Leibniz algebra, any such product can be "left-normalized": we can write it as a linear combination of products of the same elements where all parentheses are shifted to the left. E.g. (ab)(cd) = ((ab)c)d - ((ab)d)c. That this works for products of arbitrary length with arbitrary bracketings is what I call the "left-normalization lemma". It requires a clever double induction proof! Together with some collaborators, we finally formalized this in Lean! Coming soon to a Mathlib release near you. As always, the formalization was even trickier than the informal proof. For example, it's already not obvious how to formalize the set of all products of elements a₁,a₂,…,aₙ of some magma (= set with a multiplication, but no further axioms). (1/3)