I really hope machine learning will succeed in producing systems that surpass contemporary mathematicians in not only finding proofs, but also suggesting definitions and theorems to simplify a database of mathematics.
It doesn't even need to use machine learning. I have written several analyses of metamath databases to look for common patterns, and then recommend definitions or theorems to simplify things. If some expression is repeatedly used over and over again, that suggests something that should be created once for reuse.
