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.
The economics in the West feel very strained right now, and this incredible tool has come along just in time to threaten one of the last bastions of middle-class safety: white collar jobs.
Confront your leaders.
I think it’s reasonable for people to say “I like the way things were, I don’t like this new future you’re proposing, and I want to limit the technology that’s doing the thing I don’t like.”
There is nothing inevitable about AI. As a society we may decide it is fundamentally unhealthy or anti-human. We have banned or curtailed access and research for other technologies before.