Perhaps using Grobner basis for formal proofs [1],[2] could be similar to what appears here, that is during the proof the length of the terms (or polynomials) can grow and then at the end there is a simplification and you obtain a short grobner basis (short axioms).

A simple question, since • is nand, the theorem ((a•b)•c)•(a•((a•c)•a))=c, can be proved trivially computing the value of both sides for the 8 values of a,b,c. Also there are 2^(2^2)=16 logic functions with two variables so is trivial to verify that the theorem is valid iff • is nand. Perhaps the difficulty is proving the theorem using rules?, there must be something that I don't see (I just took a glimpse in a few seconds).

Automatic formal proofs can be useful when you are able to test [1] https://doi.org/10.1016/j.jpaa.2008.11.043 [2] https://ceur-ws.org/Vol-3455/short4.pdf

If I understand you correctly, you're misreading the theorem. The problem isn't to prove that statement, it's to show that if you assume that statement to be true, you get all of boolean logic.

The thing you're missing is that at no point is it assumed that there are exactly two elements in a boolean algebra. In fact you can have a boolean algebra with four elements (see https://en.wikipedia.org/wiki/Boolean_algebra_(structure)).

It seems the author is using the word logic, so logic boolean algebra suggests the classical case. Perhaps what is not trivial is that one can use that rule to deduce the other axioms. So that is not the theorem what is important but that one can prove any tautology using that simple axiom.