Comment by andybak
2 hours ago
Not a mathematician but surely if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps. What advantage is it to me to be less informed?
2 hours ago
Not a mathematician but surely if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps. What advantage is it to me to be less informed?
I can prompt ChatGPT right now and ask for mountains of more "mathematical work"; thousands and thousands of pages of nonsense for you to review. So you can "be informed".
But you couldn't make me review it. Anyway I think you're just straw manning what I was trying to say. I probably didn't express it terribly clearly and I'm not invested enough in this debate to put any more time in.
He’s not strawmanning you as much as taking OAI at their word. Plausibly the majority of the work was done with a fractional amount of human oversight, and maybe he’s sort of operating on the assumption they’re running “every” open problem continuously, which is pretty sensible. If you’re a mathematician working on an open problem which other people know about (how much of actual mathematics work is this kind of workflow varies from field to field) you can be pretty certain that an AI lab is prompting at it.
But you can't do it with their internal model that is the same or a successor to the one that solved the navier stokes millenium prize problem.
With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.
Nobody solved the navier stokes problem, Jesus. A subproblem was possibly solved (still being verified) based on context in an actual mathematician’s chats with ChatGPT. These models on their own are still incapable of producing anything but slop.
Mathematicians are in no rush. And they are less likely to review math vomit that hasn't even been formalized and verified. Especially among the now thousands of vomit papers out there.
[dead]