Theorems are not generally presented in math journals in the way they were discovered, so I am not sure machine learning from journal articles would greatly help in discovery. The issue is really that going from question to answer is a different process from verifying an answer is correct, or guiding a reader through such a verification which is what a proof is.

A perhaps less lofty, but still incredibly useful, goal would be automating a process for simplifying proofs

Or alternatively convincing mathematicians to narrate their own mental process of discovery.