It is interesting to note, apparently combining formal proof checkers with machine learning could be used to create synthetic training data for automatic self-training of proof generators. It could work something like this: https://news.ycombinator.com/item?id=38036986

Since formal proof checkers provide a reward signal (correct/incorrect proof) the above process could scale to superhuman performance in generating proofs for conjectures. This is unlike ordinary language models, which only try to imitate the human-written training distribution.