A statement that some proposition is true or false is usually less useful than a new framework for understanding the class of problem.

A machine that takes longer and longer to prove propositions in ever more inscrutable ways is hardly useful at all.

The machine too needs to produce more generalizable and comprehensible systems, for it to scale up its own conceptualization. Needing to load all the new mathematics in the context window won't be great either.