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.