Four color theorem proved by computer (1976)
Kenneth Appel and Wolfgang Haken at the University of Illinois reduced the four-color map problem to roughly 1,936 cases and checked each by computer. The result needed 1,200 hours of mainframe time. Many mathematicians refused to accept the proof because no human could verify it by hand.
Illinois began stamping outgoing mail 'Four Colors Suffice.' Philosophy journals ran years of arguments about what counts as a proof.
Computer-assisted proofs gained slow acceptance. Georges Gonthier produced a fully machine-verified version in 2005 using the Coq proof assistant, ending the dispute.
The Appel-Haken proof showed mathematicians would accept machine-aided work if it could be independently verified. OpenAI's unit-distance proof is following the same playbook with a 19-page human-readable verification paper.
