Around ten years ago Marijn Heule, Oliver Kullmann and Victor Marek proved that if you 2-colour the positive integers from 1 to 7825, then you must be able to find x, y and z all of the same colour with x^2+y^2=z^2 -- that is, a monochromatic Pythagorean triple. 1/

This solved an old problem of Ron Graham. The proof was a massive brute-force argument. Not pure brute force, since that would have been utterly infeasible, but a clever brute-force computation using a SAT solver. 2/

But I'm pretty sure it was meant humorously and not (as suggested in the Quanta article) as any kind of criticism, since I think now, and thought then, that these kinds of results are pretty cool. 4/

The joke would have been the suggestion that one might read a proof of this type as though it were a more conventional kind of argument, and complicated case analyses in conventional arguments are generally regarded as somewhat ugly. 5/

But of course a proof of this kind is not designed to be read in the conventional way, and has its own kind of appeal. Personally, I'm fine with the idea of using nice arguments to reduce a proof to a massive computation and then doing the computation. 6/

There appear to be some problems that cannot realistically be solved except by this kind of approach, in which case I see no reason not to use it, and I'm happy with the resulting level of understanding. 7/

That said, if someone were to find a proof of the four-colour theorem (for example) that didn't require a huge case analysis, I'd celebrate that and regard it as an advance in understanding, since it would explain why the case analysis had worked out, 8/

which for now I regard as something that just happens to be the case. Likewise, if somebody were to find a human-scale argument for the Pythagorean-triples problem then I would be delighted. But I very much doubt that such an argument exists, and that doesn't bother me. 9/9