The article explains that the translation from the original problem to the computer-checked problem was quite ingenious.

Turning a problem about continuous space to a graph problem, and then using a computer to check the graph problem does not kill much (or any) of the art form I would think.