Usually, during the last years, when researchers wanted to create a
machine learning-based automated prover, they used some corpus of
formalised mathematical knowledge as a training set. I always thought
that it wasn't a good idea since all these databases are relatively
small. They also are usually biased and depend on fundamentals and
exact approaches for proofs chosen by human curators. This month, a
preprint appeared of a paper written by some guys from Google where
they tried to generate a training corpus of proofs of seemingly
meaningless theorems. Quite interestingly, they managed to create a
prover that performed well on theorems from the TPTP collection. It
would be nice to create something similar to that but in my way.
