Suppose I put an ant in a tiny racecar on every face of a soccer ball. Each ant then drives around the edges of her face counterclockwise. The goal is to prove that two of the ants will eventually collide (provided they aren't allowed to stand still or go arbitrarily slow).

My brother told me about this result, but I can't quite seem to prove it. Instead of a soccer ball, we should be able to use any connected graph on a sphere (provided that there are no vertices of valence 1). We may as well assume there are no vertices of valence 2 either, since you can always just fuse the two edges.

I (and some people I've talked to) have come up with a number of observations and approaches:

- Notice that if two ants are ever on the same edge, then they will crash, so the problem is discrete. You can just keep track of which edge each ant is on, and let the ants move one at a time. Then the goal is to show that there is no way for the ants to move without crashing unless some ant only moves a finite number of times.
- You can assume all the faces are triangles. If there is a face with more than three edges, then you can triangulate it and make the ants on the triangles move in such a way that it looks exactly the same "from the outside". If there is a 1-gon, it's easy to show the ants will crash. If there is a 2-gon, it's easy to show that you can turn it into an edge without changing whether or not there is a crash.
- One approach is to induct on the number of faces. If there is a counterexample, I feel like you should either be able to fuse two adjacent faces or shrink one face to a point to get a smaller counterexample, but I can't get either of these approaches to work.
- If you have a counterexample on a graph, I think you get a counterexample on the dual graph. Have the dual ant be on the next edge along which a (non-dual) ant will pass through the given vertex.
- It feels like there might be a very slick solution using the hairy ball theorem.