There’s been some work on getting machines to try to make reasonable conjectures and definitions (see for example the work of Simon Colton) but I’m not aware of any work of actually trying to teach machines. I suspect this would be very difficult since most machine learning systems work best when the problems are in some vague sense fuzzy rather than formal.
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.
There’s been some work on getting machines to try to make reasonable conjectures and definitions (see for example the work of Simon Colton) but I’m not aware of any work of actually trying to teach machines. I suspect this would be very difficult since most machine learning systems work best when the problems are in some vague sense fuzzy rather than formal.
The problem of deciding which definitions are interesting is far from being formal.
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.