There are also interesting weak forms of the 4CT where the challenge is of course to give a direct proof. An immediate consequence of the 4CT is that every planar graph has an independent set of size $n/4$, the best known result (without using 4CT) is $2n/9$ by Albertson (1976). It is very interesting to ask about fractional coloring number. Hilton, Rado, and Scott, introduced the notion of fractional coloring and proved "A (< 5)-colour theorem for planar graphs (1973)."
We say that a graph $G$ have a fractional coloring number $t$ $(\chi^*(G)=t)$ if we can assign the independent sets of $G$ nonnegative weights such that the sum of weights of independent sets containing any given vertex is at most 1 and the total sum of weight is $t$, and, moreover, $t$ is the smallest number with this property.
Two remarkable conjectures by Heckman and Thomas are:
Conjecture 1: Every subcubic triangle-free graphis fractionally 14/5-colorable.
Conjecture 2: Every subcubic triangle-free planar graph is fractionally 8/3-colorable.
(So conjecture 1 is a strengthening of a weakening of the 4CT.)
in 2013, Dvořák, Sereni, and Volec in the paper Subcubic triangle-free graphs have fractional chromatic number at most 14/5 proved Conjecture 1!