Also I'd argue that chess's utility is ultimately the same as pure math, particularly in esoteric fields. These things are highly improbable to ever lead to any sort of real world breakthrough. The main benefit is an outlet for human logic, creativity, and exploration - which significant self improvement possible along the journey for players.
Presumably AI will be connect the dots to the applications. As the declaration says, this isn't just about math. Human understanding is losing economic value. You can understand stuff on your own time, I guess.
The standard justification for pure math to holders of purse-strings is something like "it might lead to a useful application down the road, like crypto, who knows". That looks pretty inefficient now. We have to entertain the possibility that AI can develop the math needed for any application we put to it. Eg if number theory didn't exist, we could have asked AI for a way to transit messages securely and it would maybe come up with fermats little theorem as part of its solution or maybe come up with an approach we can't conceive of right now seeing as most of us are constrained to available number theory. Like how in the last year when I give an LLM a programming project I see it doesnt even bother with of the many software libraries I and others have written and just codes up the calls it needs on the fly or finds some other ad hoc solution.
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.
What is the purpose of that?
Its like art being produced for AI to consume. What is gained from that?
And at some point AI will start suggesting - or doing - physical experiments.
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.
Yes.
Friends and I often work on Putnam problems and this series:
The (Almost) Impossible Integrals, Sums, and Series by Cornel Ioan Vălean
There's two points about this I am assuming 1) Mathematics actually has a significant subjectivity to it and is community oriented and not just climbing a never ending list of theorems that exists in the universe 2) A lot of mathematical research work is inside of a subfield and isn't directly motivated by applications. Sometimes it is but e.g. people don't work on obscure theorems about elliptic curves because of a dire need for that but more because the community found it interesting.
Does your "one" only contain humans or does it also contain other AI systems. AI math is not a single monolithic thing, but a distributed one. I see value in sharing proofs even among just AI.