[agnishom]

1. It matters because there are human mathematicians who pride themselves for their mathematical achievements. Mathematics is art to them.

2. Yes, it is. Because pre-LLM era computer-aided proofs were about using the computer to either solve a large number of cases or to check that each step in a proof mechanically follows from the axioms.

[snoman]

1. And some that are equally skilled that don’t. It matters, internally, to them but it needn’t matter to anyone else.

[agnishom]

On the flip side, there are people (like me) far less skilled that do (take joy in the appreciation of mathematics as art).