A general equality problem for Abelian groups
Consider the problem of deciding whether of deciding whether an equation, such as
$$ (x + y) + z + -(x + z) = y$$
is true in all Abelian groups. This means that for any Abelian group $A$, and for any chosen values $x$, $y$ and $z$ in $A$, the equation should be true.
This hardly poses a problem, for humans atleast - by "expanding", "cancelling", "rearranging" and "grouping", anyone well-versed in high-school algebra can solve an arbitrary instance of this problem without much thought.
However, this task is not trivial to carry out on a computer if one requires a full and rigorous proof in the end. The problem of deciding whether an equation holds in all Abelian groups is the same as deciding whether the equation can be deduced from the axioms for Abelian groups, and it is in the latter form that the task is usually presented to the computer.
The computer sees the equation not as a single line that can be read from left to right, but rather as an equality of two complicated nested expression trees involving addition, subtraction or negation operators at the nodes and variables at the leaves. This means that the computer cannot ignore the parentheses and tinker easily with the order of the variables the way humans do. A fully-bracketed version of the above looks like
$$ (((x) + (y)) + (z)) + (-((x) + (z))) = (y) $$
Any proof from the axioms becomes a complicated ordeal of shuffling parentheses and swapping the order of adjacent variables, and even cancelling adjacent terms in an expression is a challenge when they are not immediately neighbours in the expression tree. Moreover, even if one is able to produce an algorithm that proves these equalities directly from the axioms, it is unlikely that the algorithm will have a good running time (in terms of the number of variables in the expression, including duplicates).
A solution to the general equality problem for Abelian groups
It turns out that to prove that a formula involving $n$ variables is true in all Abelian groups, it suffices to show it for a specific set of $n$ elements in a specific Abelian group, namely the basis of the free Abelian group on $n$ elements ($\mathbb{Z}^{n}$).
The crucial property relevant here is that $\mathbb{Z}^{n}$ is a free Abelian group, which by definition means that any map from the basis $\{(0, \ldots, 0, i, 0, \ldots, 0) \mid 1 \leq i \leq n\}$ to an Abelian group $A$ extends uniquely to an Abelian group homomorphism from $\mathbb{Z}^{n}$ to $A$.
A worked example
The general solution is perhaps best illustrated by working out a specific example such as the one above:
Plugging in $(1, 0, 0), (0, 1, 0), (0, 0, 1)$ for $x, y, z$ in the above example yields the equation
$$ ((1, 0, 0) + (0, 1, 0)) + (0, 0, 1) - ((1, 0, 0) + (0, 0, 1)) = (0, 1, 0) $$
which is true since both sides compute to $(0, 1, 0)$.
Now consider an arbitrary Abelian group $A$, and elements $a, b, c$ in $A$. The function taking the basis element $(1, 0, 0)$ to $a$, $(0, 1, 0)$ to $b$, $(0, 0, 1)$ to $c$ extends to a unique homomorphism $\phi : \mathbb{Z}^{n} \to A$, and evaluating $\phi$ on the two sides of the previous equation gives
$$\phi\left(((1, 0, 0) + (0, 1, 0)) + (0, 0, 1) - ((1, 0, 0) + (0, 0, 1))\right) = \phi\left((0, 1, 0)\right)$$
Distributing the homomorphism across addition, subtraction and negation turns the expression into
$$(\phi((1, 0, 0)) + \phi((0, 1, 0))) + \phi((0, 0, 1)) - (\phi((1, 0, 0)) + \phi((0, 0, 1))) = \phi((0, 1, 0))$$
which is precisely the required equation
$$(a + b) + c - (a + c) = b$$
The general solution
The solution in the worked example can be directly generalised to work for any equation.
For an equation involving $n$ variables, consider the free Abelian group on $n$ generators. Verifying the equation for the $n$ generators is a matter of direct computation. This is enough to prove it for all Abelian groups, since for any Abelian group $A$ and $n$ elements $a_{1}, a_{2}, \ldots, a_{n}$ in $A$, there is a homomorphism sending the generators of the free group to these elements, and any equation involving only the Abelian group operations (addition, negation, subtraction) is preserved under homomorphisms.
Remarks
In a way, proving an equality by passing to the free group makes precise the intuitive operations of rearranging and grouping mentioned earlier. The order on the basis elements of the free group fixes an implicit order on the variables in the equation, and the normal form imposed by the tuples of integers handles grouping and cancellation of variables.
Implementation of the solution
One advantage of the approach illustrated in the previous section is that the proof is reduced to a computation that involves reducing two trees to ordered tuples of integers. This can be done in a time linear in the number of nodes of the tree, and hence linear in the number of leaves of the tree (since each node has at most two children), which is the number of varibles (with duplication) occurring in the expression.
The Lean4 programming language is ideal for this kind of mixing of programs, meta-programs and proofs, and Siddhartha Gadgil and I have implemented a rough prototype of such a tactic for solving equations in Abelian groups. This is still not ready for direct use, but the plan is to polish it up, try to implement it in various ways, and eventually push it as a tactic to mathlib4.
TODO Generalisations of the solution
The reduction of the general problem of proving an equation in all Abelian groups to the special case of the basis of the free Abelian group was certainly not specific to just Abelian groups, and it is likely that this kind of a reduction admits a more general formulation in the language of Category theory.
The correct analogue of a free Abelian group seems to be a free object in a category - the free objects in the category of groups are the free groups, the free objects in the category of rings are the polynomial rings, and so on.
Understanding the phenomenon in higher generality will likely reveal simpler ways to implement it in a system such as Lean4.