Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question

closed as too broad by 900 sit-ups a day, T. Bongers, amWhy, Hakim, Ross Millikan Jun 28 at 1:40

There are either too many possible answers, or good answers would be too long for this format. Please add details to narrow the answer set or to isolate an issue that can be answered in a few paragraphs.If this question can be reworded to fit the rules in the help center, please edit the question.

what are tptp problems? –  Jorge Fernández Jun 9 at 23:46
Can we prove that 'interestingness' can't be quantified? There seems to be types of statements that most people will agree are uninteresting, and there seem to be statements that more people than not find interesting. Some random polynomial equation demonstrating an identity with its roots is less interesting than Euler's identity. Heuristics for what is interesting and useful one might think aren't entirely implausible. –  dezakin Jun 9 at 23:59
This has nothing to do with set theory, proof theory or automated proofs. It's a philosophical question, and one that barely has any roots in the mathematical grounds it supposes to come from. –  Asaf Karagila Jun 10 at 0:02
I do not understand the close votes here. I wonder if people are hanging onto Asaf's phrase, "I also don't see how this can be reasonably answered, but that's a different story." But just because he doesn't see how it can be reasonably answered does not mean that it can't be reasonably answered. Also, I do not believe that this is a justifiable close reason... –  user1729 Jun 11 at 10:48
I have started a meta discussion on this question here. –  user1729 Jun 19 at 9:20

Browse other questions tagged or ask your own question.