Four-colour theorem

Four Color Theorem

Model / AI: Computer-assisted search (no ML)

computer-assisted proof by Appel and Haken; formalized in Coq by Gonthier and Werner (2005).

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Context — Four Color Theorem
• Formal proof — Gonthier and Werner (2005)