Formal Proof—The Four-Color Theorem.¶
Gonthier, G. (2008). Formal Proof—The Four-Color Theorem. Notices of the American Mathematical Society, 55(11), 1382-1393.
Cited by¶
4 citations across 4 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Verifier-Prover Asymmetry
- Mathematical proof shows the same gap: finding a proof can take decades while refereeing it takes weeks, and proof assistants sharpen the asymmetry by certifying a proof object cheaply.
This sourceA machine-checked proof object verified cheaply by the Coq kernel — only the theorem statement need be reviewed — illustrating proof assistants sharpening the find-versus-verify gap in mathematics.
- Mathematical proof shows the same gap: finding a proof can take decades while refereeing it takes weeks, and proof assistants sharpen the asymmetry by certifying a proof object cheaply.
Domain-specific¶
- Computer-Assisted Proof
- Four Color Theorem
- These are grounds for the guarantee, distinct from the graph conditions to which it applies.
This sourceStates the map theorem on printed p.1383 and the connected-open region, adjacency and corner definitions on printed p.1388, Definitions 2–4. The official article was inaccessible directly; a complete 12-page published-layout facsimile from Cornell was inspected, including the relevant definition page. This is the 2008 published article, distinct from the undated 57-page report A computer-checked proof of the Four Colour Theorem. No Coq proof rerun is claimed. Segment-sharing shorthand is restricted to ordinary polygonal maps; the constructed square example is derived from the published definitions.
- These are grounds for the guarantee, distinct from the graph conditions to which it applies.
Mechanisms¶
- Proof Assistant Script
- The famous demonstration that this scales is real: the four-colour theorem was fully verified in Coq
This sourceDocuments a large-scale, fully Coq-verified proof of the Four-Color Theorem.
- The famous demonstration that this scales is real: the four-colour theorem was fully verified in Coq
Verification¶
Does it exist? Not checked yet. This entry carries no identifier to resolve. It was extracted from the citation as written in the article, normalized, and deduplicated against the rest of the registry.
Does it back the claim? Not recorded. Neither this nor any other of the 4 citations of this work carries a recorded support check.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:e93a29b030ab · see in the full table