the assumption is "understanding" is something distinct from abstraction, compression, generalization, which are what theorem finding does. I would argue theore

the assumption is "understanding" is something distinct from abstraction, compression, generalization, which are what theorem finding does. I would argue theorems are understandings. What does understanding mean otherwise in a non-circular way? Cultural significance? Mathematicians feeling threatened by automated math seems like a cultural issue to me not an understanding issue at least on the machines' side.