A non-empty binary tree is either made of a single node (the root) or is determined by the two trees below the root.
This means that, as a type, the type T of binary trees satisfies the "equation" T=1+T^{2}.
It can be checked that, as an equation concerning complex numbers, this equation has sixth roots of unity as its solutions.
This indicates that, in some way, we may expect to have T=T^{7}.
This actually holds for trees, but a proof of the isomorphism can't involve any minus sign, since types can't be substracted.
In other words, we have to work in the semi-ring ℕ[T]/(T=1+T^{2}), and we wish to prove T=T^{7}.
This game is related to this problem in the following way:
This means that every move in this game corresponds to a completely explicit isomorphism of types.
By reaching the state corresponding to the polynomial T^{7}, the player demonstrates a result, made famous by Andreas Blass:
The type T of binary trees is "very explicitly" isomorphic to the type T^{7} of septuples of trees.
Note that, as a player, you're making your own proof of the result when playing this game.
Different players will construct different bijections...
This is a fun way to solve the computational part of the theorem!
Here is a link to the famous paper "Seven Trees in One" by Andreas Blass, on the arXiv: https://arxiv.org/pdf/math/9405205.
Game by Béranger Seguin, december 2021.
A funnier version of the game ;).
The (dirty) Python code used to prove that 18 moves are necessary.