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 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.