A famous theorem by van der Waerden states the following: Given any
finite coloring of the integers, one color contains arbitrarily
long arithmetic progressions. Equivalently, for every q,k, there is
an N = N(q,k) such that for every q-coloring of an interval of
length N one color contains a progression of length k. An
obvious question is what is the growth rate of N = N(q,k). Some
proofs, like van der Waerden's combinatorial argument, answer this
question directly, while the topological proof by Furstenberg and
Weiss does not. We present an analysis of (Girard's variant of)
Furstenberg and Weiss's proof based on monotone functional
interpretation, both yielding bounds and providing a general
illustration of proof mining in topological dynamics. The bounds do
not improve previous results by Girard, but only—as is also
revealed by the analysis—because the combinatorial proof and the
topological dynamics proof in principle are identical.