Mehdi Mhalla et Frédéric Prost: Preuves et jeux d’échecs
La résolution de la valeur théorique de jeux populaires comme les dames, les échecs, othello, le jeu de Go etc. est un challenge informatique particulièrement intéressant. Du fait de la taille des espaces considérés (autour de 10^45 positions légales pour le jeux d’échecs par exemple) les recherches en force ne peuvent aboutir. Il faut donc trouver des stratégies de preuves plus subtiles. Récemment, en 2007, le jeu de dame a été prouvé comme étant une nulle. La construction de la preuve a pris plus de dix ans, et a nécessité des centaines d’ordinateurs en occupant une place mémoire gigantesque. En utilisant une nouvelle approche nous avons pu montrer que le jeu d’échecs sur un échiquier 5 x 5 (Gardner Chess) est également une partie nulle. Alors que les espaces de recherche des deux jeux (dames et échecs sur 5 x 5) sont du même ordre de grandeur (autour de 10^19 positions légales) notre preuve est humainement lisible (une dizaine de pages) et a été réalisée avec l’aide d’ordinateurs personnels. Nous montrerons comment cette approche peut être automatisée et généralisée ainsi que les perspectives que nous envisageons.