[pfortuny]

Mathematics is a language for humans, not just for machines. We may agree to let machines "do their thing" for as long as they want but to what purpose? Just creating "results"? What is a mathematical result by itself?

Unless, of course, we are willing to give machines the responsibility of building bridges. Subject on which I do not have a clear opinion yet.

But just hard drives (or whatever) filled with bytes representing strings representing nothing any human will ever understand... I am not for it (as of now). There are much more important problems to solve.

[nilkn]

I'm not sure why we would assume that AI-generated or AI-assisted mathematics would never amount to anything useful in the real world. I would expect the opposite: the usefulness and explanatory power of mathematics has been riding an exponential over the last several centuries.

Maybe I didn't do a good job explaining it, but the rest of my prior comment was about connecting AI-generated results back into human-style thinking. Inevitably, in the far future, it's not unreasonable to assume the world will be dominated by synthetic robots controlled by artificial intelligence, and there will indeed be a point where AI builds not just bridges but vast planetary, interplanetary, and space-based infrastructure projects beyond the ability of our current civilization. At that point, mathematics may permanently move beyond the grasp of the human species. You can't teach a dog general relativity. Surely, there are truths in mathematics (and possibly physics) you cannot teach a human. Not to digress, but for me, this kind of threshold is what a term like "superintelligence" means -- the point where an intelligence is discovering truths that cannot be taught back to humans because we're not smart enough. So far, our contact with this kind of intelligence has been limited to one-off, highly specialized cases (like chess) that have little grand implication for civilization, but that won't always be the case.

But, for today and probably at least our lifetime, to make them useful major AI advances in math will need to be "compressed" back into the specific network and "towers" of concepts and abstractions that human minds specifically can understand and intuit about. So I think both directions of formalization are equally important: translating natural language statements (theorems, lemmas, etc.) faithfully into Lean and letting a theorem prover run and decoding a dense Lean proof back into natural language (which, in some ways, is the more creative and open-ended problem -- there is no one right answer).