3 ms·
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 manip
by juped 6y ago
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.
- cthonicthulu 6y agoThis is a take that I generally agree with. To be honest, I kinda feel the same way about breathless think-pieces talking about GPT-3.
- orange3xchicken 6y agoMany 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".
- juped 6y agoGood thing I never claimed that, I just said it was uninteresting to mathematicians unless it has artistic merit!