Question: 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.

Answer: 
This is known as Klyachko's Car Crash Theorem. It was proved in order to prove a theorem about finitely presented groups. In fact, the result allows the ants to move at arbitrary nonzero speeds so long as they make infinitely many loops around their 2-cell. The conclusion is that there's either a collision between ants in the interior of an edge, or else there is a `complete collision', which means that there's a collision at a vertex of all ants from adjacent edges. 

EDIT: Oh, it's actually important that there are **two** complete collisions, which is somewhat harder to prove than one (a collision in the middle of an edge is also a complete collision.)

You can read an expository article by Colin Rourke [here](http://msp.warwick.ac.uk/~cpr/ftp/klyachko.ps).
A quick comment on the idea of "a very slick solution using the hairy ball theorem". Any such *very* slick proof will surely only use the fact that the Euler characteristic is non-zero, and so should apply just as well to surfaces of higher genus (at least two). For instance, if I understand it correctly, then Reid's answer above would work just as well on a higher-genus surface, by the Poincare--Hopf Theorem.

But the theorem does **not** hold on surfaces of higher genus.

What follows would probably be better with pictures, but I'll try to describe it without and hope for the best.

For instance, it's easy to divide a torus into two rectangles such that there are "traffic schedules" with no crashes. (OK, the Euler characteristic of a torus is zero, but bear with me.) (Also, what is to ants as a traffic schedule is to cars?)

Now consider the surface of genus two as an octagon with sides identified, as usual. You can divide this into two rectangles and two pentagons in a way that mimics two copies of the torus picture in the previous paragraph: the surface is the union of two tori with boundary, and each torus is divided into a rectangle and a pentagon. Schedule each torus as before (stretching one of the ants' route over the fifth side of the pentagon). As only one ant from each torus traverses the fifth side of the pentagon, it is easy to arrange that the ants from different tori do so at different times.

Does that make sense, or does anyone want a picture?

EDIT:

Oh, and of course it follows that the theorem is also false on any orientable surface of even higher genus, as they all cover the surface of genus two.