In some sense "understanding" (understanding if it is true, if it is important, how to use it) is about the only bottleneck in math. Any theorem that you can write down or imagine is already true, false, not provable already. In some ways we can already start iterating through all the theorems. We will never get to the end (or really get very far down the line) and most all of them be trivial (I think the Busy Beaver[1] project is a fascinating example, ymmv).

I am wary of AI in all aspects I am seeing it in but in many ways in mathematics seems to me the least troubling. It will change things in and the field will not be the same. Blacksmithing has not really gone away. You can still work as a farrier, if you like that sort of things. The tools that replaced a man working over a forge with a big hammer are part of a giant industry that is still producing works for the modern world.

[1]: https://bbchallenge.org/8226493

Chasing these 'trivialities' is a good thing, imo.

The Busy Beaver game has lead to a better understanding of complexity theory and automata. Also, direct "hands on" work on improving proof assistants and related tools.

Btw, for those who are curious, the Busy Beaver Challenge wiki is a treasure trove of rabbit holes and curiosities:

https://wiki.bbchallenge.org/wiki/Main_Page