The Four Colour Theorem: The first time machines mogged mathematicians

The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.

the title made me think of a much older machine that was used for calculating

https://en.wikipedia.org/wiki/Antikythera_mechanism

I think a lot of great ideas like tree-width were developed in hope of simplifying the proof.

I didn’t know we had invented time machines yet. ;)

I think the same happens now with AI generating code. Nobody will read every line. that's part of the process from now on.