Are mathematical proofs by computer legitimate? Already 50 years ago, Appel and Haken proved the century-old four-colour problem with thousands of case distinctions that could only reliably be analysed by computer. A very simple special case (no computer needed) is the three-colour theorem: a map where every country has an even number of neighbours can be coloured with three colours so that countries with a common boundary line have different colours. Planar maps are also the surfaces of polytopes such as cubes or tetrahedra, and when colouring their faces, their multi-coloured corners are a natural representation of so-called Nash equilibria in two-player games. This connection is the topic of this talk.

The three-colour theorem can be used to show that there are games with three strategies for one player (and any number of strategies for the other player) that have the maximum possible number of Nash equilibria. Games with more strategies give rise to polytopes in higher dimensions, and here we needed computer help to solve a 25-year old problem on the maximum number of Nash equilibria of a game with five strategies on each side. An upper bound is 42, and for the corresponding „dual neighbourly“ polytopes a full list of 159,375 combinatorial types can be checked with suitable obstructions that their maximum equilibrium number is 32. But further tricks are needed for more general polytopes where no such list exists to show that this is the true bound.

This research is joint work with Constantin Ickstadt and Thorsten Theobald (University of Frankfurt).