] The Four Colour Theorem, proposed by Francis Guthrie in
] 1852, states that any four colours are the minimum needed
] to fill in a flat map without any two regions of the same
] colour touching.
]
] A proof of the theorem was announced by two US
] mathematicians, Kenneth Appel and Wolfgang Haken, in
] 1976. But a crucial portion of their work involved
] checking many thousands of maps - a task that can only
] feasibly be done using a computer. So a long-standing
] concern has been that some hidden flaw in the computer
] code they used might undermine the overall logic of the
] proof.

Once again, coq to the rescue.