Yes, it makes me think of the 4-color map theorem.

It also makes me think of Gödel's theorem.

Which leads me to contemplate a theorem generating system that takes a set of axioms, generates all of the theorems in that system, compares them to a list of proven results in various systems, and determines which results can't be proven with those axioms (and the subset that are actually contradicted).