One of the projects I'd like to work on over the next several years in my spare time is a first order theorem prover similar to Prover9 to attack some of the TPTP problems, and it occurs to me that there should be a way to generate interesting conjectures or flag generated lemmas that are mathematically 'interesting' in some way. The problem, of course, is how do you define 'interesting?'
Basically, anyone who's had any experience with formal logic or automated theorem proving will note that most well formed formulas, and even most theorems, aren't interesting; They're one of the infinite number of ways to rewrite an obvious identity, they're useless tautologies, or they're a mindlessly huge expansion of a simple expression obtained with term rewriting. One of the things I was wondering about is if there's any way to quantify what an interesting statement is in any way.
If we had some way of quantifying interestingness, I could generate interesting conjectures and then search for a proof of their truth or falsehood, then add them to a set of support for proving further theorems, and lemmas generated from theorem proving could be tested for their 'interestingness' as well.
Some of the notions I've been thinking about is brevity (after applying definitions) as we often value statements that can be written simply, and utility... how often a lemma is used as a supporting statement to prove another 'interesting' statement. But I don't really have more than guesses about heuristics for what should make a statement interesting and what makes a statement dull or useless. I certainly don't know how to quantify interesting definitions to create things like arithmetic from set theory.
Is there more to be said about quantifying what is interesting and what isn't?