Comment by yurimo
1 day ago
I think it is important to divine what currently AI is good for and what it is not even in such verifiable environments like math. Current hyped announcements about breaking conjectures are notable and are a marker of how much improvement was made. But as I read them, and maybe I am wrong, I see it as a large model+ harness executing a broad brute force search and trying solutions until something sticks. There are lots of problems like that and they should be solved, as often they are perhaps less important or overlooked, or just a slog, any field of research has these, math even more so.
However, this is very different from inventing new mathematical machinery that allows to break old problems, I think it will be a while until AI will be able to do it if at all. For now I think we will be moving to a symbiosis where an AI cracking a problem and giving a solution, inspires a human to invent new techniques.
Agreed, AI is not capable at the moment of coming up with radical ideas to solve the tough problems. Sadly, I would argue many problems in math are likely to be found to be not actually tough in this sense, and those working in "comfortable" areas with fewer tough problems are having real crises of their own right now.
But even for the tough problems, it is good at executing on a particular idea with reasonable competency. It's also quite decent at verification now. That can radically speed up proof development overall, since those aspects can become quite tedious otherwise.
finally someone is saying it our loud lol. mathematicans are just finding lower and upper bounds and having a computer input them into a theorem prover more times than a human is able to on their own. ai imo isnt solving anything.