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.
Does anyone know of work that attempts to build a theorem prover by learning-from-examples? I'm imagining extracting a large corpus of theorems from back issues of mathematical journals, then applying unsupervised structure discovery techniques from machine learning to discover recurring patterns.
Perhaps a model of the "set of theorems that humans tend to produce" would be helpful in proving new theorems.
The unsupervised-structure-discovery bit does seem within the realm of current machine learning.
Any references to related work?