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.