And the goal of computer mathematics research is computer understanding of mathematics. I fail to see a reason provided as to why society should defund automated reasoning just so mathematicians can put off burger flipping for another year.