Similar formulas in terms of n th roots have been known since the 1500s for equations with degrees n up to 4, although their LeafCount starting at n = 1 increases like 6, 25, 183, 718. … For degrees 5 and 6 it was shown in the late 1800s that EllipticTheta or Hypergeometric2F1 are sufficient, although for degrees 5 and 6 respectively the necessary formulas have a LeafCount in the billions. (Sharing common subexpressions yields a LeafCount in the thousands.)

The shortest single axiom currently known for lattice theory has LeafCount 79 and involves 7 variables. But I suspect that in fact a LeafCount less than about 20 is enough.

[Enumerating] possible expressions LeafCount[expr] gives the number of symbols that appear anywhere in an expression, while Depth[expr] gives the number of closing brackets at the end of its functional representation—equal to the number of levels in the rightmost branch of the tree representation. … With a list s of possible symbols, c[s, n] gives all possible expressions with LeafCount[expr]  n : c[s_, 1] = s; c[s_, n_] := Flatten[ Table[Outer[#1[#2] &, c[s, n - m], c[s, m]], {m, n - 1}]] There are a total of Binomial[2n - 2, n - 1] Length[s] n /n such expressions.

The longest tautology at step t is Nest[(# ⊼ #) ⊼ (# ⊼ p t ) & , p ⊼ (p ⊼ p), t - 1] whose LeafCount grows like 3 t .

Combinator properties The size of a combinator expression is conveniently measured by its LeafCount .

The total number of recursive functions grows roughly exponentially in the size ( LeafCount ) of such expressions, and roughly linearly in the number of arguments. … But given an enumeration of primitive recursive functions (say ordered first by LeafCount , then with Sort ) in which the m th function is w[m] diagonalization (see page 1128 ) yields the function w[x][x] shown below which cannot be primitive recursive.

From this representation of Power the universal equation can be converted to a purely polynomial equation with 2154 variables—which when expanded has 1683150 terms, total degree 16 (average per term 6.8), maximum coefficient 17827424 and LeafCount 16540206.