So then it sounds like you agree that math has additional utility beyond just human comprehension.

If I understand you correctly, you're just qualifying that that will only be the case when AGI exists. To be clear, I actually disagree with you here because I think it's very plausible to find a use case for human-incomprehensible math proofs before AGI exists. I'm just saying it sounds like you're agreeing with the parent comment that math is not purely about human comprehension.