Tao's proposition could be read completely differently depending on if you care about solving open problems OR about (pure) mathematics as a field. I think many commenters are in the former group, hence missing the point. The takeaway here should be that proof-maxxing via AI is particularly destructive to the (pure) math ecosystem because in many cases the process (both successful ones and failed ones) is just as important as the proof. When AI is hyper-optimized on finding the most "correct" path to arrive at a solution, you fail to look at all the other possible paths. They might be less "correct" or "efficient" but could also yield more interesting results that will inspire other problems or fields. Judging from the history of mathematics, without trials and errors that happened when the math community came together to focus on one single hard problem, mathematics wouldn't be as diverse and abundant as what it is today. With AI, we risk removing all of these trials and errors such that, while in the short term might mean we solve open problems at 100x speed (depth), could significantly impair the breadth of mathematics as a field.
What feels sad to me is that for many people though, this doesn't matter / the incentives don't line up to do anything to this situation, especially if you're applying math in your field. In this case, AI being hyper-optimized on finding the best solution / proof does indeed benefit those people enormously.