[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.