Four Color Theorem proof by Appel and Haken sparked 1976 backlash over computer math
In July 1976, mathematicians Kenneth Appel and Wolfgang Haken, aided by programmer John Koch, proved the Four Color Theorem using roughly 1,200 hours of computer processing and 10 billion logical decisions. The achievement, the first major theorem proved with heavy reliance on a computer, drew sharp criticism from mathematicians who argued that a proof no human could fully verify by hand should not count as legitimate mathematics.