I wonder if someone could make some standardized way to describe/write mathematical proofs - in a very formal language and then train a model that will try to find more proofs for open questions.