As a sibling of your comment points out, "opposition to AI's convenience" is not Tao's position. He has used LLMs to help with the problems he's talking about -- https://terrytao.wordpress.com/2026/07/21/a-digestion-of-the... and https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the... turn opaque straight-from-the-model results into things that can be understood.
The Sendov example has a piece coders will hopefully recognize: he found a formalization that was 1/6 the amount of code of the original one. And the analogy with code goes further--the messy version will run/pass the proof checker, but the one that's been cleaned up and made sense of is a better foundation for future work. That's true even for future LLM-assisted work.
So it's not about whether mathematicians take advantage of LLM help (Tao favors that) but, more or less, whether the point of math is just to make a bigger version of the GitHub dump vs. everything else: readability/comprehensibility, negative results that fill in the map around a problem (not just 'lighthouse' theorems), organizing results to plan out future work, and so on.