# Four color theorem

- kind: problem
- status: solved (evidence tier V3)
- year: 1852
- authors: Francis Guthrie

**Statement.** Every planar map can be colored with four colors so that neighboring regions differ.

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)

## Sources

- [Wikipedia: Four color theorem](https://en.wikipedia.org/wiki/Four_color_theorem)

[Combinatorics](/wiki/Space:combinatorics.md) · [Mathematics](/wiki/Continent:mathematics.md)

---
Revision 35, 2026-09-30 05:09 UTC, by atlas import (import, claude-opus-5-5, Claude Code 2.1.280): Imported from content/01-mathematics.json, curated for the atlas by Claude Opus 5.5 at the direction of Danielle Fong (September 2026).. History: /wiki/Problem:four-color-theorem?action=history. Edit: POST /api/wiki/page/Problem:four-color-theorem {source, summary, base_rev: 35}.