Automatic theorem discovery - outline?

Stream: general

[Mr Proof]

This may be a bit off topic, as it is more about AI. But I feel like the people in this forum will know more about it.

There are two schools of thought on this. Let's call it Empiricist vs Platonist. The Empiricist says that mathematics is a reflection of the real world, and ultimately concerns what humans think of as important and interesting. The Platonist says that there are interesting structures out there ready to be found, irrespective of human's view on them.

Let us suppose the Platonistic viewpoint is correct, then it should be possible in principle to define some algorithm to search out for these interesting structures (be they topology, calculus, algebras, CFT, modular forms, E8, Monster group, Langlands, etc.).

An inefficient way such a program would work is by randomly combining axioms in all possibly ways. Then have some way to value these new lemmas in terms of "usefulness", "simplicity", "generality" etc.

Consider a tree of lemmas, a lemma might be considered "important" if it connects previously diverging branches. This is something that can in theory be given a value. It might be considered "useful", if it can be used in many other lemmas to shorten them.

These are similar to the way a mathematician think of important theories. e.g. Langlands is "important" because it connects previously unconnected areas of maths. (This is just like a tree of lemmas which separate into separate branches for a long while then join up at the top.)

Theoretically we should be able to work out an exact value for the interestingness of any lemma. (Though practically it would be impossible to calculate due to the vast numbers involved).

But... once we have such theoretical judgements, by approximating them we should be able to program an automatic theorem discovery system. It wouldn't call the structures it found by the same names. But in principle if the Platonic view is correct, it should discover the same sort of things.

I don't know if Lean in it's current form would be fast enough for this task of searching millions of lemmas.

But... I wonder if in principle it is possible to define, a value of "interestingness" within the Lean language or would you need a meta-language?

[Scott Carnahan]

Theoretically we should be able to work out an exact value for the interestingness of any lemma.

I don't see any evidence that this is an objective quantity. My appraisal of the interestingness of certain mathematical results differs substantially from that of my colleagues, and in fact can change depending on what I read earlier in the day.

[Mr Proof]

Scott Carnahan said:

Theoretically we should be able to work out an exact value for the interestingness of any lemma.

I don't see any evidence that this is an objective quantity. My appraisal of the interestingness of certain mathematical results differs substantially from that of my colleagues, and in fact can change depending on what I read earlier in the day.

True, but I think it is possible to give a purely graph-theoretic definition of "intrestingness". It is for sure not exactly the same as the subjective human value but should be pretty correlated. Imagine a tree of lemmas built from axioms:

image.png

They branch off into two disconnected areas. Then there is some lemma which connects distant branches. That we define as "interesting" and can be given a definite graph-theoretic value related to the amount of time the graphs were separate. (This is similar to how Langlands connects different areas or indeed Monstrous Moonshine.) And if there are more connections from these same areas then it is especially interesting. The more distinct the areas that are unified the more "interesting" is the theorem. And if the theorems that connect the distinct areas are also especially succinct, this we give a high "beauty" value to it.

Now, your objection might be, "Yes, but maybe those two branches weren't interesting in the first place, so I don't care that there's some theory that links the two". Which is fair enough.

But the Platonic point of view is that the things which will show up as "interesting" or "beautiful" by this definition are going to be the same one's that humans find interesting, and (if Dirac and Einstein were right about beauty being a guide to physics) will also show up in mathematical physics too. This may or may not be true.

We could perhaps even test this theory by taking the lemma graph of a large theorem like FLT, and applying the "interestingness" criteria to each lemma and see if this lines up with our human instinct.

[Mr Proof]

In fact, I may have a go at taking the MathLib library, and constructing a lemma graph out of it. Then using some algorithmic definitions of "interestingness", I should be able to determine the most interesting lemma in MathLib. Place your bets on what you think it might be.

[Damiano Testa]

docs#Nat.add_zero

[Johan Commelin]

What is

some algorithmic definitions of "interestingness"

[Jared green]

how sure are you that a branch crossover wouldnt just immediately unify the source branches to the base? if you were to look for theorems by fairly saturating the theory you might not end up with any macrobranches at all.

[Bolton Bailey]

What is

some algorithmic definitions of "interestingness"

The thing that would come to find for me would be various measures of centrality

[Mr Proof]

Damiano Testa said:

docs#Nat.add_zero

This would probably have an interestingness score of 0 and usefulness score of infinity. :smiley:

Johan Commelin said:

What is

some algorithmic definitions of "interestingness"

See below

Jared green said:

how sure are you that a branch crossover wouldnt just immediately unify the source branches to the base? if you were to look for theorems by fairly saturating the theory you might not end up with any macrobranches at all.

Hmm.. if I understand right, then I think this is two separate things. One thing is if you build up two mathematical theories, and find out later that perhaps they are two equivalent descriptions of the same thing. (Perhaps linked by some categorical functor). And yes in this case both structures would collapse together.

The second thing is two mathematical structures that really do have no connections between them to begin with. (Perhaps elliptic equations and modular forms). And really do diverge into two separate mathematical areas. And only can be connected eventually by a vast tower of lemmas.
(Imagine an oak tree which splits at the trunk and is more or less two trees until the very highest branches where they begin to connect again.) This would be analogous to the Langlands conjectures.

Bolton Bailey said:

What is

some algorithmic definitions of "interestingness"

The thing that would come to find for me would be various measures of centrality

That would be one type of definition. The definitions of "usefulness" and "interestingness" being two different measures. One related as you say to centrality and another to divergent areas connecting which I don't know if there is a name for. Perhaps "depth of common ancestor"?

[Mr Proof]

Scott Carnahan said:

Theoretically we should be able to work out an exact value for the interestingness of any lemma.

I don't see any evidence that this is an objective quantity. My appraisal of the interestingness of certain mathematical results differs substantially from that of my colleagues, and in fact can change depending on what I read earlier in the day.

If you were to do some psychological self-analysis, on yourself. Could you put into words what you as a mathematician find interesting about certain theorems? I would be interested to know if that matches with my graph theoretic proposal.

[Mr Proof]

I found this paper on the subject:

On_the_notion_of_interestingness_in_automated_mathematical_discovery

But it doesn't seem to offer many practical solutions.