Comment by lwansbrough
17 hours ago
It would be nice if one of these models would produce a novel theory or advance the field in a positive direction.
Most (all?) of the big discoveries have been counterexamples, which is just sort of a systematic tearing down human ingenuity. I know that counterexamples are an important part of progress and discovery, but it just feels bad to me.
But I'm not a mathematician, maybe I'm totally misreading the vibe.
Not all, see the cycle double cover conjecture proof: https://mathstodon.xyz/@tao/117207849921390904
We will have to see whether any other millennium problems fall. I guess that in a year the scope of AI math will be much clearer, for now it's still a bunch of incidents of unclear pattern.
Nuts that Tao literally predicted the exact strategy openAI seems to have used not even a week ago
Since he wrote this five days ago, when these efforts were already underway, if he was not Terence Tao I would suspect he had inside access. But since he said he did not and was speaking hypothetically, and he seems to be an honest person as far as I can judge, I guess some people are just on another level.
this isn't really true anymore. First, a number of the big results are constructions, not counterexamples. For example the existence of a non-sofic group. It was widely believed that non-sofic groups existed (so it wasn't a "counterexample" to a widely believed conjecture), but no constructions were known.
There are other examples though. For example, NP hardness of n^{1/400}-approx CVP. Like any NP hardness proof, this shows you can faithfully encode a hard problem (3SAT here iirc) in terms of another candidate hard problem. Not really a counterexample at all.