Mathematics is about discovering and understanding the logical implications of assumed axioms under various inference rules.

Alternatively, some claim that mathematics is about understanding these implications.

Under the first definition, AI is already, and forevermore will be faster and better at proving theorems. Just like it is better at checkers, chess, and now go.

The author asserts that AI proofs are incomprehensible to humans, and so under the second definition AI is merely a tool to overcome one hurdle on the way to understanding.

So which is it? The author seems to claim the second definition, but bemoan the end of mathematics under the first.