Comment by juped

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.