Comment by PowerElectronix

It looks to me more like they made a math engine that can sift through a huge number of combinations, most them absurd, to prove a statement. Just like a chess engine, but for math.

At least that's what I get from the NS result, they got from a point close to the solution to the solution by making it churn through 10 million bucks of compute.