[frakt0x90]

This is something I've been thinking about a lot lately. Especially in combinatorics and number theory, there are databases like oeis, LMFDB, etc that contain tons of data with the ability to generate more algorithmically (sometimes easier said than done). Using ML to get heuristics and really good guesses on where the next opportunities lie and then formalizing it once you have a good guess would be SO cool.

Is there a name for that? Or groups working on that stuff that I could follow?

My own little pet project was I scraped OEIS and built a graph of sequences where 2 were connected if one mentioned the other in its related sequences section. You got these huge clusters around prime powers and other important sequences. Then I thought maybe you could use a GNN to do link prediction providing an estimation of a relationship that should exist but hasn't been discovered yet.

[ykonstant]

The Lean 4 Focused Research Organization has ML interoperability in its roadmap. Since Lean 4 is shaping up to be a capable general purpose language as well, I can imagine a Lean project that retrieves and formats LMFDB data, uses it to train and test a NN, gets Lean 4 proof code from it, verifies or rejects it (possibly with more detailed feedback) and loops this like a "conversation".

However, Lean 4 still has a long way to go in terms of speed and library features, and I at least have given up on writing optimized code until we get the new compiler (whose timeline seems optimistic to me, but Leo de Moura knows much better).

[knotthebest]

At which point would mathematicians become obsolete? Something like this seems like it could automate a lot of mathematics research, no?

[ykonstant]

We would be interested in actual automation of theorem production, but this pipeline would automate approximately 0% of (interesting) mathematics research. It does have the potential to automate some boring parts and enable mathematicians to make better conjectures faster.

[knotthebest]

I think I may be missing something. Why would you be interested in the automation of theorem production? Wouldn’t this make mathematicians obsolete? How far away do you think we are from that?

I ask as a newbie in math; math is a passion of mine. I am genuinely reconsidering going into math research as I fear just being automated away.

[joachimma]

I am not a mathematician but have some interest on a pop-sci level. I believe this presentation at G-Research by Alex Davies would be of interest. https://www.youtube.com/watch?v=Mp_skPK-X9M

[goodmachine]

IANAM but I guess the name for mining OEIS or generating scads of data iteratively for analysis would be empirical mathematics.

It's empirical metamathematics if you attempt this with networks of axioms/theories

https://www.wolframscience.com/metamathematics/empirical-met...

https://writings.stephenwolfram.com/2020/09/the-empirical-me...

[jononor]

In these area of physics informed machine learning this is refered to as "discovering new physics". Probably there are analogs in computational mathematics, biology, chemistry, etc.