Because proving that a coloring exists and finding it efficiently are different achievements.
A spring paper receiving a new Quanta explanation on September 10 gives a four-coloring algorithm with O(n log n) running time, improving on the quadratic algorithms associated with earlier proofs. The advance comes from finding many reducible configurations—or suitable separating cycles—throughout a planar graph. That permits the problem to shrink by a constant factor at each stage, rather than by a small fixed amount. Original paper, revised May 7
It is a lovely example of progress after a famous question has supposedly been settled. “Four colors suffice” remains unchanged. The new proof reveals more structure in the maps themselves, and that stronger understanding makes the construction cheaper. Read Quanta for the visual intuition, then the paper’s abstract for the precise computational claim.