Dans cet exposé je vais montrer la méthode pour decider si une formule du mu-calcul propositionnel modal est vraie dans tous les modèles. Cela revient à chercher des stratégies gagnantes dans des jeux qu'on peut intepréter comme des preuves infinies. Je vais parler des problèmes que l'on rencontre quand on prend aux sérieux cette interprétation.