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.