Kenneth Appel

So it takes until 1976.

This is work by Kenneth Appel and Wolfgang Haken, and they do indeed use computers, although actually a mix of computers and really, really rigorous hand-done calculations, and they come up with this unavoidable set that's more than a thousand configurations in the end.

And each one of these is what mathematicians call reducible, which means that you can always show that you can remove it from the graph, you can change some of the colorings of the graph, and then you can put it back in and always use only four colors.

So basically in 1976, they come out with this massive proof with all these calculations, with all this computer code, and people are pretty skeptical.