> Automated theorem proving is the only way to build better machines.

Sure, but that will just be one aspect of an integrated and wholistic AI, which can configure the parameters input to the automated theorem proving component, and act on the results.