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: 
The post consists of initial ideas on top and **the proof** at the bottom.

---

I think the key idea is to perform the process opposite to what you describe about subdividing into triangles. Indeed, our problem can be thought of a plane graph where all ants are moving in the counterclockwise direction except one on the outer circle which goes *clockwise*.

Now notice that it seems you can actually combine several areas into one, it should look the same or worse on the outside, and you get at the end two ants on the same circle moving in the opposite directions.

"The same or worse" part is conjectural, but the intuition is that assuming you have just two circles with common edge, "the best" you can do is to let one go through the edge then immediately after that let the next one proceed. If you think about how that affects the outside world, it's very similar to having a single ant going around the whole stuff.

---

**The proof.** Let's introduce some notation. First, I'll be considering ants on the plane which together form something with an outer circle. Now let's assume the ants have decided upon the schedule and they started their driving. The outer ant is *drunk driver* that goes in a clockwise direction.

We will prove that the crash will necessarily occur before the drunk driver makes a full cycle. 

> 
> **Crucial lemma.** Suppose I have two areas A and B combined by an edge and a schedule of driving that includes drunk driver making a full cycle. Then it's possible to choose one of the areas, A or B, and the modification of route of drunk driver that makes a full cycle around the chosen area.
> 
> 
> 

The lemma is established by drawing a picture (update: an answer that refers to a paper with the solution was posted. the answer is the same so you can read the corresponding description there). After you have the lemma, you're done, because you see that there must be a simple face (minimal area) with a sober and drunk ants which must crash.
Say there are n faces. The phase space on which the ants are moving are on is T^n, and the ants movement is described by a curve on T^n that has speed bounded from below in any direction. Hence, it suffices to show that if you cut T^n along the collision loci, you reduce the dimension of the H^1. This is a purely combinatiorial claim, which (it seems - I did not check all the details) you can prove by induction.