Vladimir_Nesov comments on Automated theorem proving by learning from examples

[Vladimir_Nesov]

The problem of deciding which definitions are interesting is far from being formal.

[Alex Flint]

Yes, and the problem of deciding which lemmas to prove and in general what structure to try for a proof is also far from begin formal. Verifying a proposed proof is the formal bit.