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.
Again I'll have to agree with timtyler. Formalizing mathematical proofs is difficult, see my old post. Maybe you'll find it easiest to use an existing corpus, like Metamath.
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?