Computer assisted proof is not a new idea. The most famous example is the four color theorem, which (as far as I know) does not have a humanly understandable proof. For this particular proof, it looks like the computer assisted part would be similar to writing down hundreds of pages of checkable inequalities. One way to do this is to use interval arithmetic, which always guarantees the answer is within the a certain given interval.

Mathematicians have split opinions about computer assisted proof. On one hand, there doesn't seem to be a real difference between one page of checkable inequalities vs 500 pages of checkable inequalities. On other other hand, computer assisted proof do not help humans gain clarity on the logical process. The fear is that the computer result will just be an "one and done" result, which people believe is true, but cannot build upon because they don't fully understand it.