A constructive topological proof of van der Waerdenʹs theorem Original Research Article

The theorem of van der Waerden on arithmetical progression is a classic result in combinatorics. While its original proof was of combinatorial nature, it was shown by Furstenberg and Weiss that this theorem can be derived from topological dynamics. This last derivation is non-effective, and it is an interesting proof-theoretical problem to extract the computational content of this topological proof. This has been done by Girard using Kreiselʹs no counterexample interpretation. Here, we give a direct constructive formulation of this topological proof, using basic notions of point-free topology.