Anyway, I agree that people like to focus on the elegant parts. Math popularization materials have too much kawaii math.
It has been proven using a computer. The problem was first reduced to a few hundred cases, then a brute force algorithm was used to solve each case.