Have you got a link to someone pointing it out? It looks like they're still going through formal proofs so likely found the problems that way.

> With automated math that community as tao pointed out is at risk.

If they can be automated, they are not necessary. If they are necessary, they won't be fully automated. It's a pretty simple experiment to run, the math "community" should bear with us. Darwin would be proud.

I didn’t read the paper but can’t this just be additionally with doing the actual muls? Or was it a nonconstructive proof?

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?

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.

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

Looks like those are new formalizations of existing proofs, not new ones

They try to be clever and put company name as the author.

I think it's equal parts PR stunt and negging.

People won't want to seriously peer review an AI study unless it's already out there potentially spreading misinformation

These are not mistakes.

Those results were not dumped to advance math. Those results were dumped to generate positive press for OpenAI.

Now it's on actual mathematicians to figure out whether the proofs are bogus or not. But the mistakes will never reach the same level of public attention as the original positive press, so for OpenAI this is good anyway, consequences be damned.

In a sense this is a microcosm of AI usage in the wild, ignorance is laundered through LLMs, and it is left for those that still have knowledge to figure out what makes sense.

OpenAI is a horribly negligent company. The threat it poses to humanity is not that their models will be a superintelligent singularity that will take over the world, is that their negligence and greed has real world consequences that they really don't give a fuck about. Like right now, their shitty math bruteforce is just keeping actual specialists occupied trying to figure out what is bullshit from what is not. For free, mind you.

SMBC had a funny take on the Good Will Hunting AI joke, recently.

https://www.smbc-comics.com/comic/equations

This is weirdo pseudo-neo-religious slop.

This metaphor might be applicable if the AI slop machine was in fact producing novel output. It seems to be getting invalidated as people dig through the wall of meaningless text surrounding the actual results.

It's so funny to see people on Hacker News talk about academic communities that they clearly are not part of. To be clear to anyone reading, no, retracting papers is _not_ standard in math. In math, people submit papers after they have checked with colleagues, they give seminars, they submit it for peer review, etc. It is not shotgunning papers and retracting incorrect ones on the regular. Retracting papers is rare and embarrassing.

Would you care to share your research? What was your methodology? Did you write it up? Is it published?

Or is it the kind of research you'd prefer to keep shrouded in mystery?

The withdrawn papers were not lean verified nor claimed to be.

Can you point to where that defense has been made?

Where are you getting unpaid from? Almost all people who are qualified to analyze the results are paid researchers. And if it is unpaid, then it sounds like they're looking it over for their own reasons, and that's fine?

I also fail to see the issue you have with releasing abandoned source. In what world is that bad? That obviously is a gift and should be encouraged. e.g. id software's history of doing that has meant their work stays alive forever.

I’m unsure. The whole academia is built on unpaid human efforts. Journal writers are unpaid, and institutions paid for their papers to be published by for-profit publishers. Journal reviewers are paid the bare minimum, certainly unproportional to their efforts and expertise.

We are all reverse centaurs now.

But have you formalized every single one of your results? And if you haven't what odds would you put on one of them not working out, if formalized?

But is it equivalent to withdrawing post-publication or is it more akin to not passing peer review with major revisions requested?

Most mathematicians don't produce 400 papers in a 48 hour window either so I'm not sure comparisons are helpful

The onus is on formal verification when it comes to computer generated results. So far only 22% of the papers have it.

Retraction and withdrawal are different. Retraction is when you publish something, it passes peer review, is published, and some time later its publication is undone, often by an editor or some other person because some fraud was uncovered.

Withdrawal is akin to submitting a paper to peer review and then when you’ve noticed mistakes, you decide to take the paper back and correct it.

Reject is when someone else notices the mistakes and tells you to take it back and correct it.

Withdrawal and reject happen all the time in a scientist’s career. They don’t necessarily mean the scientist is doing bad research, just the research was not ready. Retract usually means something more.

By dumping the papers, OpenAI skipped the typical peer review process, so peer review should be understood as what’s going on now as mathematicians look over the papers and find flaws.

Irresponsible is an adjective that means lacking a proper sense of responsibility, or acting without thinking about or caring about the potential consequences of one's actions.

They do not care if they waste everyone’s time or flood the common with slop. They did not spend their own time to verify that the Lean proofs correspond to the natural language proofs. They did not even spend their own time to verify that all of these proofs are well written.

They instead are mining the unrenewable resource of open math problems.

However, seeing it another way is easy if you are financially motivated by their upcoming IPO (see how easy it is to invent motivations for comments?).

It is irresponsible when nobody checked it for correctness first. They just copy pasted what the slop machine spit out.

it's like if you vibe coded something and the onus is now on the reviewer and the reviewer tells you your work contains bugs and is messy - that is not acceptable from the reviewers pov - why should the reviewer spend all his human effort, a scarce resource, reviewing your code while you've spent barely a fraction of his effort generating this. OpenAI is a trillion dollar company, surely they can verify stuff before pushing it out? The problem is not that they are solving the problems, they don't care at all about the actual process of doing mathematics. Using compute to mine problems and throwing results in github and letting human reviewers spend effort to correct these is not going to win them any favor. If OpenAI really cared about math, they would have someone on their side who actually understood the results they produced and was able to verify their correctness and educate others.

Withdrawing it isn't irresponsible. I don't even think releasing it is, because that is often the best way to find problems with it; expose it to the wider research community. Doing PR victory laps based on unverified, unfinished work, on the other hand, is. It is well known, even scientifically demonstrated, that retractions or refutations get much less attention than the initial exuberant PR announcement. And thus this practice contributes to misinformation.

And just to preempt the kneejerk whataboutism: Yes, all of academia does this to varying extents, and the mainstream media are also complicit. And that is also irresponsible. And no, that is not an excuse for OpenAI. Especially when you consider that OpenAI actively portray themselves as some kind of moral arbiter on AI and "doing good for humanity". They should be held to the extraordinarily high moral standards they purport to hold themselves to.

They only withdrew it after someone pointed out that it was a flawed paper.

In one case by asking Astra to review it.

Not exactly encouraging that they did their homework before publishing results.

Withdrawing it, in itself, might not be, but it kind of skips over the part where they have a paper that warrants it in the first place.