Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments
Two independent Lean 4 proofs of the Four Color Theorem, each following Gonthier and Werner's Coq proof and each written almost entirely by a Claude model under one person's direction, resting only on Lean's three standard axioms.
- Lab
- Independent
- Model
- Claude Fable 5.1 and Claude Opus 5 (Emery); Claude Opus 5.5 (Barish)
- Field
- Mathematics
- Date
- 2026-09-16
- Human collaborators
- Chris Emery, Robert D. Barish
- Problem posed
- 1852 · open 174 yrs
What was found
Chris Emery's corun1024/4ct, public on 2026-09-16, proves FourColor.fourColorTheorem from a 195-line statement file that transcribes Gonthier's real-plane statement and proves its elementary topological notions equal to Mathlib's IsOpen, closure and IsPreconnected. Its README reports 115,342 declarations checked with no sorry and no extra axiom; its reducibility certificates are produced by C and Python tools and then checked by the Lean kernel. Robert D. Barish's port, public on 2026-09-26, transcribes Coq's realplane.v one for one in a 220-line Challenge.lean and computes all 633 reducibility certificates inside Lean during the build, so the Lean toolchain alone checks it. Its README reports a local rehearsal of Palomar's pipeline in which leanchecker, nanoda and con-ron accept the proof, and it carries a Palomar registration. Neither development uses native_decide.
Novelty check
This is a formalization of a known theorem, not new mathematics, and is graded as such. Appel and Haken proved the theorem in 1976, Robertson, Sanders, Seymour and Thomas gave a simplified proof in 1997, and Gonthier and Werner machine-checked it in Coq in 2005; both Lean developments follow that Coq proof. A web search and the two READMEs found no earlier complete Lean 4 proof: Barish's README names Emery's as public before his own, and Emery's repository was created on 2026-09-16, ten days before Barish's. The 2026-09-28 watch run surfaced only Barish's port, through its Palomar registration.
Caveats and known objections
No human has reviewed either development. Barish's README says the final comparison of the statements against Gonthier's was done by a separate Claude Opus 5.5 agent that had not written the proof, and Emery's asks readers not to take the theorem on his authority or the model's. The checks recorded are the authors' own runs; nothing here has been rebuilt. Graded claimed rather than formal, following this registry's practice for Palomar-registered proofs: a registration shows the proof typechecks against a recorded statement, not that the statement is the theorem, and no third party has audited either statement file. What would move the grade is small by design, since each statement is about 200 lines of elementary definitions. Autonomy is ai-led rather than autonomous because in both cases a human set the goal and constraints and ran the final builds, while the disclosures credit the models with essentially all of the code.
Machine-checked elsewhere
PalomarPALOMAR-2026-09-27-000005
RBarish-UTokyo/FourColorTheorem-Lean4 at 20fa34599f51 · checked 2026-09-27
ProvedFourColor.RealPlane.four_color
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Covers Barish's port only; Emery's development carries no registration.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-16-four-color-theorem-leanBibTeX
@misc{whataifound-independent-2026-lean,
title = {Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-09-16-four-color-theorem-lean}
}