Difference between revisions
four-color-theorem
Source +0 −0
… 26 unchanged lines
Revision 35 as rendered
It was the first major theorem proved with essential help from a computer, which checked 1,936 configurations. Many mathematicians refused to accept a proof no human could check. Robertson, Sanders, Seymour and Thomas simplified it in 1996, and Georges Gonthier checked it completely in Coq in 2005, which ended the argument.
Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.
Posed 1852, Francis Guthrie. Closed 1976, Kenneth Appel and Wolfgang Haken; formalized in Coq 2005.
What would settle it
Formal proof in Coq (Gonthier, 2005)