As is well known, planar graphs are four-colorable. It turns out that this is a lower bound only if the graph contains triangles. In 1959, Groetzsch showed that triangle-free planar graphs can be 3-colored. In 1994, Thomassen produced a shorter and easier to understand proof of this and extended it to results on triangle-free graphs on the torus and the projective plane. I will present Thomassen's proof for the planar case and discuss how a polynomial-time algorithm might be drawn out of that.
This is part of work in progress towards (I hope) a linear time algorithm.
Note: I have a copy of Thomassen's paper for anyone interested.