The 4 color theorem was a boring case analysis, but that doesn't mean that all computer proofs are boring and tedious.
We have proof assistants using many beautiful type theoretic languages, and tools which can (attempt) to write proofs in this languages.
In fact, this is one of the best usages of ML because we hardly care whatever impenetrable bullshit goes into the proof search when the proof must be self-justifying, and, just like a ML go game log, potentially lead to new techniques for human mathematicians.
We have proof assistants using many beautiful type theoretic languages, and tools which can (attempt) to write proofs in this languages.
In fact, this is one of the best usages of ML because we hardly care whatever impenetrable bullshit goes into the proof search when the proof must be self-justifying, and, just like a ML go game log, potentially lead to new techniques for human mathematicians.