> Since nobody would pay for random points in theorem-space, it must have some way of figuring out what the human brains down at the breaker box actually want.

Would a machine learning approach be possible? For example, has anyone built a generative model, trained from theorems (and proofs) from math texts or formalized versions thereof?