Last I checked (a few weeks ago, but things have been moving faster lately), the four-color theorem remains "computer proved". There has been work done on it since the original proof that has successfully simplified it, in the sense that those proofs involve less grinding through cases than the original. But it still involves grinding through more cases than can be sensibly labelled a "human comprehensible" proof, with some sort of insight into the problem space. It's still just a big set of cases being checked, and a useful final result, but no insight given in the proof.

This seems like an interesting test case to build up for AI models.