Choosability version of Thue's theorem on nonrepetitive sequences

Pattern avoidance is a deeply studied problem within the field of combinatorics on words. One of the seminal results of this area is the theorem of Thue which asserts that there exists an infinite word over three letter alphabet, in which no two consecutive substrings are identical. A number of proofs of this fact are known. Few are as simple as the original one. Most of them, however, illustrate techniques which can be applied in other contexts.

A variant of the problem, that we are interested in, is called the choosability version. In that case the alphabet is not fixed but for every position of the sequence the choice of symbols is (independently) constrained. If for each position we can chose a letter from a set of size at least four, then it is always possible to construct an arbitrarily long nonrepetitive sequence. It is a challenging question whether such a sequence is guaranteed to exist if there are only three options. First result of this kind was obtained by Alon, Grytczuk, Hałuszczak and Riordan in 2001 by an application of Lovasz Local Lemma. All consecutive improvements (on the sufficient number of options) was obtained by more refined applications and more specific variants of the lemma.In a sense, for some time, this problem served as a benchmark for probabilistic local techniques.

We are going to discuss another proof of Thue's theorem and perspectives of generalising it in a way that would allow to improve the results on the choosability version of the problem.
The approach combines so called entropy compression argument with approximation of the language of nonrepetitive words by regular languages.