I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?

I suggest "Catching crumbs from the table" by Ted Chiang. Very short piece published in Nature (2000) and well worth a read. Depicts a scenario where modified humans produce science beyond ordinary scientists' comprehension.

Mochizuki enters the chat