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.

Just dropping a comment here to let y'all know I'm all out of time, but yeah, I would definitely put more time into reading hundreds of pages of slop proofs if it was my field, but sorry I really have to run right now.

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.

That's not what this is about. The person I was responding to said "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". That's what I was responding to. They were basically suggesting that the amount of mathematical slop in the world should be maximized, and then it would be up to humans to choose what they would want to read. You know, a needle in a haystack type of thing, where you're maximizing the size of the haystack.

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.

I think it's more likely the millions of dollars of compute than the model, in many cases.

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.

Apparently the write-ups are garbage (as in very hard to read). I feel like they could've had AI fix that up at least somewhat. Maybe they'll reinvest more in writing ability now.

The write-ups are one thing and more of a cherry on top but I would say the more pressing matter is the lack of Lean formalization which means you can't really say it has been (dis)proven or not.

I didn't check but I thought they included lean certificates. That seems like an obvious thing to do. How do we even know any of this is right?

I think the obscurity is a feature, not a bug. They don't want a headline where 250 of these results are invalidated overnight. They want rejections to trickle out and be buried.

Not sure why you're being downvoted, because this is exactly what I think is happening.

My man, there are more than 100,000 professional mathematicians in the world.

Are they all too busy having brilliant ideas? Doubt.

OpenAI math paper dump should be considered like a hint from 200 IQ eccentric genius - unreliable but perhaps insightful. If it was not "ugh AI" people would be happy about it.

Right. Imagine if some human mathmetician released what OpenAI did with all the caveats and warnings about possible mistakes.

It would be ridiculous for anyone to say "hey man you really shouldn't even have posted these unless you have an ironclad proof".

Humans make mistakes all the time, including in mathematics papers.

Almost like they care less about the maths and more about a deadline for marketing purposes.

The whole modus operandi for LLMs at this point is to produce a flood of material and then hope someone else will have to do the hard work of verifying it while you gloat about your productivity.

I mean I somewhat agree that only the formalized results should be taken seriously, but I don't really think that openai has an obligation to do so.