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.

Type

Journal article

Intellectual base

Primary research

Year

2008

Link

https://www.ams.org/notices/200811/tx081101382p.pdf

Cited from

mathematics

Cited by

3 citations across 3 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.

Domain-specific

• Computer-Assisted Proof
  • The human contribution supplies the theorem, reduction, algorithm, mathematical justification, and interpretation; the computational contribution discharges a portion that is impractical or impossible to survey manually.

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.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:e93a29b030ab · see in the full table