{"id":247877,"date":"2026-09-09T09:59:48","date_gmt":"2026-09-09T14:59:48","guid":{"rendered":"https:\/\/www.johndcook.com\/blog\/?p=247877"},"modified":"2026-09-09T09:59:48","modified_gmt":"2026-09-09T14:59:48","slug":"four-colors","status":"publish","type":"post","link":"https:\/\/www.johndcook.com\/blog\/2026\/09\/09\/four-colors\/","title":{"rendered":"A 50-year-old computer-assisted proof"},"content":{"rendered":"

The idea of using computers to assist with proofs is not new. The first major computer-assisted proof was published in 1976, the proof of the four color theorem by Kenneth Appel and Wolfgang Haken. The authors reduced the proof of the four color theorem to verifying calculations on 1,834 configurations, each checked by a computer program.<\/p>\n

The proof was simplified over the years, and formalized in Coq in 2005. Everyone is satisfied that the theorem is true, but there has never been a satisfying proof, one that a human could read and say “I see now why any map can be colored using only four colors.” And there may never be one, but see this post<\/a> for a contrary prediction.<\/p>\n

The IBM mainframe that ran the calculations completing the proof of the four color theorem did not generate the proof. It simply executed the FORTRAN program that Haken and Appel (and Koch [1]) gave it.<\/p>\n

I don’t see the recent proof of finite-time blowup for solutions to the Navier-Stokes equations as entirely different. Computers did higher-level tasks for the OpenAI team than the mainframe did for Haken and Appel, and these tasks were not as directly programmed as the tasks that were given to the mainframe, but still machines do what they are told to do.<\/p>\n

Related posts<\/h2>\n