alt Hacker NewsI get the impression that the value of unproven conjectures is more in the new math and techniques that may be discovered - by humans - trying to prove/disprove them, rather than much utility in any eventual result.
Take something like Fermat's last theorem - I'd be curious to hear of any use of the result itself, but there was a massive amount of new mathematics generated by those working on it, whether ultimately successful or not.
These AI math proofs are interesting testament to the power of reinforcement learning applied to math, obviously reflecting the axiomatic self-consistent nature of math itself, but it doesn't seem they have the same value as a humans working on these problems since they are using known math to solve them rather than inventing anything new.
However, it would still be interesting to analyze the LLM lines of reasoning that lead to any of these results, since there may be value there even if no new math, just as human Go players have found value in analyzing computer Go.
Still, as Demis Hassabis has himself said, the real goal with AI is discovery and creativity - you want to create the thing that could design the game of Go in the first place, not just play it. Similarly with math, while there is interest in seeing an AI "play math" using the rules of the game, what would be of much more interest is the AI that can create new math, in the same way as Andrew Wiles did while proving Fermat's last theorem.
Replies
> are using known math to solve them rather than inventing anything new.
Isn't a new proof new math? If not, what qualifies as new math?
It just occurred to me that this "it's not the destination, it's the journey", what you learn and contribute by trying to solve a problem, may point to what I'm guessing is an unpopular conclusion...
It may actually be a negative, rather than a positive, for AI to have solved these problems.
If humans had continued to work on these problems, then its quite possible they may have invented new math along the way and benefited the field. Now that the problems are solved, in one manner, I would assume that the level of human interest in them is much diminished, and the likelihood of these problems generating the same benefit for mathematics has diminished. Erdos chose his problems precisely because he thought they could advance the field.
AI itself does not appear to have benefited from solving these problems - they are hard for a human but apparently fairly easy for an AI. We don't just have one result here, proven after great labor, but 10 (with more results rumored to be withheld), with the effort/cost to generate them reported to be low.
The temptation to announce AI solutions to problems that are hard for humans, easy for AI, may be hard to resist, but perhaps there would be more benefit to be had to leave the hard for human problems for humans to solve, and be more impressed when AI solves problems that are hard for AI.
As Hans Moravec noted "What's easy for humans is hard for computers, and what's hard for humans is easy for computers", and while AI is trying to make inroads into that, it still remains fundamentally true.