En julio de 1976, Kenneth Appel y Wolfgang Haken publicaron la primera prueba del Teorema de los Cuatro Colores, un resultado matemático que había confundi a los expertos durante más de un siglo. La demostración, que afirma que cualquier mapa puede colorearse con máximo cuatro colores sin que regiones adyacentes compartan el mismo tono, dependió en gran medida de la verificación computacional. El sistema de Appel y Haken realizó 1.200 horas de cómputo y tomó 10.000 millones de decisiones para validar el caso crítico, marcando el inicio de la era de la matemática asistida por máquinas.
La recepción de la prueba entre la comunidad matemática fue dividida. Mientras figuras como Bill Tutte y Heinrich Heesch aceptaron el resultado, otros matemáticos, como Herbert Wilf y Paul Halmos, rechazaron la validez del método, argumentando que la verificación por computadora constituía una 'oracle' matemática y no un razonamiento lógico tradicional. Algunos incluso negaron la existencia de la prueba, comparándola con el 'traje del rey'. La credibilidad se consolidó con el tiempo gracias a la aceptación de otros expertos y la publicación de un artículo de opinión en The New York Times, aunque inicialmente los editores se resistieron a cubrirlo por temor a que fuera una falsa alarma. Este evento sentó las bases para el debate filosófico sobre la naturaleza de la demostración matemática en la era digital.