Comment by vrighter

That computers can be used to perform long calculations is nothing novel. That is literally what they were designed to do.

The 4 color theorem was proven because humans actually did the math and discovered a way to simplify the problem enough for them to write a program that proves it. The proof wasn't discovered by a computer. The proof was discovered by the people who wrote that program. There was no machine learning involved.