> (The prover won't derive an invalid proof, it will just fail to derive a valid one.) I don't think there are many applications of machine learning that have this property.
Don't basically all applications of any heuristic solver to NP problems have this property? (Including problems that are only in NP, because they are also already in P.)
Yes, sure, I could have phrased that better. There are no doubt many possible applications of the idea. The recent headline-grabbing applications of machine learning tend not to be like this.
Though even amongst the recent-headline-grabbing stuff there are some areas that you can improve at by the equivalent of AlphaGo's self-play. Basically, when you have a slow and expensive option to use a weaker version of your system to produce better decisions / smarter data, and then use those to train the system.
Don't basically all applications of any heuristic solver to NP problems have this property? (Including problems that are only in NP, because they are also already in P.)