Hacker News Reader

Comment by fidotron | Hacker News Reader

> It's a bit like a tree falling in a forest. If an LLM proves a theorem but no one understands it, did it make a sound?

But in future most proofs will be for consumption by other AI models in the pursuit of yet other proofs.

It's kind of surprising so many mathematicians act surprised by this given this was clearly where automated proof assistants would lead. I guess they assumed they'd always be the ones guiding them.

View on HN

> But in future most proofs will be for consumption by other AI models in the pursuit of yet other proofs.

What is the purpose of that?

Its like art being produced for AI to consume. What is gained from that?

Well if it proves useless presumably they'd stop doing it.

But if AI is to recursively self improve understanding and evolving its own foundations, which are clearly mathematical, is essential. There is no need for humans to grasp what is going on in that loop.

Math also has applications, and they don't rely on human mathematicians doing the math.

I mean, was the point of math ever just because some humans enjoyed doing it? Even though a lot of it is theoretical, there's been all sorts of useful things that have come out of it as well due to an improved understanding of the universe through new ways of thinking about it. If it got to the point where no human could understand it and there were no ways to actually use it, I don't think anyone would bother having their computers doing it at all.

wouldn't AI solving problems in science, engineering, economics, etc be able to apply the new AI math?

Yeah, that's kind of my point. I would have to imagine that the people investing in AI doing math (using "investing" loosely, not just financial but hardware/energy/opportunity cost as well, which may or may not seem roughly equivalent to money depending on your viewpoint) would just stop unless it remained possible to apply in some way or was understandable by humans.

> was the point of math ever just because some humans enjoyed doing it?

Yes.

Friends and I often work on Putnam problems and this series:

The (Almost) Impossible Integrals, Sums, and Series by Cornel Ioan Vălean

You can enjoy math, but that was never the only reason people in general did math. (It was the only reason for some people, sure.)

Your claim confuses me. This history of math is replete with people doing it for the love of the game.

As I said, these people exist. And math is fun!

But it's far from the only reason people in general do and have done math.

What would stop you from doing that if AI happened to be doing a bunch of different or more advanced stuff? I assume that the fact that there are humans doing other or more advanced stuff doesn't dissuade you from doing it for fun?

It's going to be hard to compete with something that has access to all of math at once and can find connections between elements that appear unrelated to humans.

And at some point AI will start suggesting - or doing - physical experiments.

Presumably some of the proofs will have applications beneficial to humans beyond impressing other mathematicians, and AI will surface them, or use them directly.

Reply on news.ycombinator.com