> I do think one core aspect of the practice of mathematics has been in increasing human understanding of it, not merely compute things with symbols.

The road towards better (in the sense that they can be "more trusted") computer-checked proofs of the four-color theorem has also lead to a better (human) understanding of the four-color theorem.