It is nice to see some sanity back in the conversation!

I'm still not sure about math-2.0 (humans+AI will make fundamentally more progress):

- AI and computer usage take a mental toll on humans and humans will overlook radical improvements.

- AI may be good at finding useless things like "P==NP, but the complexity is O(n**4242424242424242)". In other words, useless.

- Humans become formalists and lose traditional sources of inspiration. Maybe interacting with Lean should be left to specialists, but not to creative blackboard mathematicians.

- AI exposure will further intellectual conformity, more than the Internet did.

As to the last point, a lot of progress (real, not measured in publications) seems to have been made when communication was slower and there were several different schools and approaches.

There is definitely a kind of monocrop problem in some fields, where it seems like having a very diverse spread of academic investigation is needed to have enough diverse traces through the search space. And globalization has been flattening that.

[dead]