{"id":"palomar/PALOMAR-2026-09-27-000005","url":"https://github.com/RBarish-UTokyo/FourColorTheorem-Lean4/tree/20fa34599f5189dd569d96dd22f306c94ab1c446","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-27-000005-v1.json","repo":"https://github.com/RBarish-UTokyo/FourColorTheorem-Lean4","tags":["math.CO","msc:05C15","msc:05C10","msc:68V20","msc:68V15","graph-theory","four-color-theorem","lean-formalization","formal-verification"],"score":0,"title":"The Four Color Theorem (Lean 4 port of Gonthier's Coq proof)","trust":"high","domain":"math.CO","source":"palomar","authors":["Robert D. Barish"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 and Mathlib formalization of the Four Color Theorem, ported from Georges Gonthier's Coq proof by Claude Opus 5.5, Anthropic's AI model, working as an agent under the direction of Robert D. Barish. The main theorem, FourColor.RealPlane.four_color, states that every simple map of the real plane can be colored with at most four colors so that adjacent regions get different colors. The map may have infinitely many regions, bounded or not; each region must be open and connected, and two regions are adjacent when their closures share a point that lies in the closure of no third region. As…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-27","reactions":{},"formalized":true,"formalizes":[{"title":"The four-colour theorem","identifier":"doi:10.1006/jctb.1997.1750","relationship":"formalizes"},{"title":"Formal Proof—The Four-Color Theorem","identifier":"https://www.ams.org/notices/200811/tx081101382p.pdf","relationship":"adapts"}]}