In the 1970s, a remarkable thing was done; a computer was used to solve a math problem. This, in and of itself, was not remarkable. The difference engine could do it. But this problem was the first one that would probably remain unsolved if it weren’t for computers.
Even during the 1970s, when computers were harder to come by and problems were weightier, computers were routinely brought in to solve things for the people who had access to them. But prior to 1976, they weren’t required to prove any math problem. They just made things easier. That is, until Kenneth Appel and Wolfgang Haken used a computer to prove a 124-year-old conjecture. In 1852, Francis Guthrie came up with what’s known as the Four-Color Theorem. That theorem stated that no map needed more than four colors to delineate territories. Generally, different countries, states, or provinces, were given different colors on a map. If a mapmaker were armed with four different colors, there was no territory, or set of them, that could be arranged in such a way that two adjoining territories were the same color.
No one had found anything to contradict Guthrie, but then no one had the time to check. Thousands of different cases would have to be tested before anyone could come to a conclusion. The theorem just wasn’t practically testable, and so not provable, by humans. In 1976, though, a human didn’t need to work through all those cases. Appel and Haken enlisted the help of a machine that worked fast and didn’t mind if its time was being wasted, and proved the Four-Color Theorem. Mapmakers raised a bored eyebrow and continued to use however many colors they felt like using. Computer scientists, though, were impressed.
via What was the first math problem that we needed a computer to solve?.