I have this feeling that the frontier of maths is going to accelerate faster than humans can keep up with it, even if machines get exceptionally good at math exposition. There’ll be some event horizon of new discoveries which are so complex we’ll never understand their intermediate steps. Beyond that point, humans will revert to “Math 1.0”, where we’ll need to rediscover proofs that have already been solved by machines, and we’ll have a pair of frontiers each for the humans and the machines.