This seems similar to bootstrapping theorem provers. Here is a HN discussion on one: https://news.ycombinator.com/item?id=21358674