I guess the problem with many Computer Assisted Proofs is that they don't explain "why" something is true, only that something is true. But if that's the best you can do, then it's certainly better than nothing.

Also, advances in CAPs can have applications outside of pure maths.

Finally, CAPs are not common enough - or viable enough in most cases - to make a dent in the practice of pure maths. At least that's the impression I get.

I think one could only claim destruction if there was evidence that other forms of math were in decline due to computer-aided proofs.

As much as we hear about computer-aided proofs and theorem proving software here on HN, these topics are still somewhat niche in mathematics as a whole.

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.

I guess if a human can't do it and a computer can, then no, it's not. What would be the other side to that argument?

I think the art is moved from the proof itself to translating the proof to computer language.

Edit: typo