Math is and has always been a form of expressive art, but there's been a vocal constituency since at least the early 20c that claims it's bloodless symbol manipulation. Since computers excel at bloodless symbol manipulation, one would expect them to be programmable to generate proofs of propositions; this is uninteresting to mathematicians unless it has some artistic merit.
Many mathematicians would disagree with the claim that automated proof checking/generation (see COQ & this presentation by Voevodsky: https://www.ias.edu/ideas/2014/voevodsky-origins) and involved techniques (see the entire field of sat & smt solvers) are "uninteresting & without artistic merit".
