The four color theorem from graph theory is certainly the most famous problem for which so far only a brute force computational proof exists. A new preprint of Kronheimer-Mrowka supports an approach towards this theorem via homology theories.
Kronheimer. Mrowka: A deformation of instanton homology for webs, https://arxiv.org/pdf/1710.05002.pdf
The four color theorem says that every planar map can be colored by four colors such that adjacent countries correspond to different colors.
It is known from Tait‘s work in the 19th century that the four color theorem is equivalent to the existence of Tait colorings on bridgeless trivalent graphs in the plane. Here a Tait coloring is a coloring of the edges by 3 colors such that each vertex is adjacent to 3 edges of different colors. A bridgeless graph is a connected graph which can not be disconnected by removing only one edge.
In an earlier paper, the authors used a variant of the instanton homology for knots to define an invariant of trivalent graphs in \({\mathbf R}^3\) (which they call „webs“). They prove that it is non-zero for bridgeless graphs, and they conjecture that it is equal to the number of Tait colorings of the graph. (Kronheimer, Mrowka: „Tait colorings, and an instanton homology for webs and foams“, https://arxiv.org/abs/1508.07205)
In the new paper, the authors construct a deformation of their homology theory for which they can actually show that its dimension agrees with the number of Tait colorings. The dimension of the deformed homology is at most that of the original homology theory. Of course, to prove the four color theorem one would need the opposite inequality.