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.