Many mathematicians would disagree with the claim that automated proof checking/generation (see COQ & this presentation by Voevodsky: https://www.ias.edu/ideas/

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 https://www.ias.edu/ideas/2014/voevodsky-origins) and involved techniques (see the entire field of sat & smt solvers) are "uninteresting & without artistic merit".