Early sentiments are a lot of the write ups still read like slop and it feels very rushed and not very polished.

I wonder if the issue is that not many people within OpenAI can validate the output. Therefore what reads well looks good, and then was published.

If that’s the case in a way its a similar delusion that average people are experiencing with their own AI use.

This is almost certainly the case. I very much doubt that anyone there of any importance in the decision-making process around this actually cares about the math, just the headlines they can get from pushing it out.

I am starting to think do they have some metrics or KPIs that they are trying to fill with this stuff. Pressure to produce anything that at least on first glance sells... Then again they probably are not only place doing that with AI...

I am certainly experiencing what seems like some mania or computer addiction from these technologies. I’ve never been able to produce such results as I can today. I lose sleep staying up late working on it (though to be fair this has always been an issue). But the volume of work is so hard to audit. It makes it difficult to make flawless results. That doesn’t excuse the mode of publication. They could have had humility in their announcement. “We are seeing some interesting results and seeking community validation.” Maybe they did, I did not read their full announcement. But that would have been the right move if they can’t verify something fully.

I've tried reading one of these, it was an unreadable mess with some strong smells. It might have something to it, but it'd take a decent amount of labor to validate it, especially with how many references to other papers it had.

Yeah imagine being in a company where everyone is suffering from AI psychosis and fully bought in. They give you unlimited tokens and tell you that you are a genius and can solve anything. You’d publish all sorts of made up slop papers.

That’s the danger isn’t it. If you’re told everything you do is going to change the world, but you’re ignorant of the output… then that’s a lot of hot air and false promises propping things up.

You could almost draw a comparison between that and inexperienced consultants making business changes, claiming glory and then disappearing before the thing falls apart.

Yes, of course. Wasn't that the whole point? To get more humans involved earlier in the process, with more transparency?

Just the other day I was thinking, if unsupervised maths will descend into "oops we found a bug in some code, branch XYZ of maths is no longer true".

If you go far enough to the edge that's already how math works, since everything is very interpretation-sensitive.

There is however a new problem of scale. Erdös was a human and still managed to create work for an entire generation of mathematicians, how much of a mess will an automathician create?

> automathician

I vote for "automathon"

c.f. Italian differential geometry

*Algebraic geometry

ha, of course -- in my defence I'm an analyst, all geometry looks the same to me ...

Sure but if the results have practical implications then the validity will be self evident. If they do not, not much of consequence has been lost.

Interesting that math gets so much attention, when actual advances to material science, biology and chemistry have much higher ramifications and economic benefits. I assume progress there is kept under wraps until they can capture the economic benefits. If they can do that, then the insane valuations may actually be valid.

> I assume progress there is kept under wraps until they can capture the economic benefits. If they can do that, then the insane valuations may actually be valid.

Or progress is not as straight forward in those fields as in math.

that's my experience (at least for experimental quantum materials research). LLMs help a lot with paper discovery, grant/paper writing etc., but on the experimental side, they barely move the needle for now. Some analyses are done faster now than they were before because you don't need to fiddle around with the code, but that's it.

In a field where a single person can maybe produce and characterize a single sample per day, AI will only really start speeding up progress once you combine it with robotics.

Were the withdrawn ones actually Lean-checked or not? seems like that matters

I’m a little confused - I thought their proofs were all driven by Lean proofs - is that not right? So even if the quality of the work is low in some metrics, it either passes the test or not..? No space for changing your mind either way.

No, in their original blog they wrote:

> As part of our GitHub repository, we are sharing formalizations of many of the proofs in Lean, a programming language that allows mathematical proofs to be checked by a computer. We will update the repository with more formalizations as we obtain them.

Meaning they published all results before checking all of them, and intended to add more Lean proofs later. In the linked post they state ~42% of the posted results now have formalized proofs, some were added, some verified, and I assume this means that some results turned out to be wrong.

This is extremely disappointing. It means they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them, while so-called "accelerationists" surf on the hype and help with the pro-AI propaganda.

If your AI tool can help advance mathematical research, share the tool with mathematicians. Using it like this is irresponsible.

"AI will kill us all": no. Greedy humans will kill us all. With AI.

Every option is going to lead to someone shitting on OpenAI for what seems to be a pretty huge accomplishment. There have been opinions written by some mathematicians that OpenAI should just share the work that they have now so that people who are working on any solved problems can know. Which seems reasonable to me.

It’s a funny one. I’m not sure what a Lean-less LLM proof even is. LLMs are amazing at bullshitting and skipping key steps and details. I’d imagine a LLM non Lean proof to be generally hard to evaluate - harder than that of a human mathematician perhaps. And the scale effect is against OAI here - the firehose just keeps squeezing out proofs.

Technically,Godel showed you can make proofs say anything. all LEAN does is proof consistency. It does not validate the starting blocks.

It’s not unreasonable to want OpenAI to be thorough and rigorously check their work before sharing it though. Sounds like that didn’t happen here.

If say 10% of papers have mistakes, I think they are thorough enough for this kind of volume and complexity.

With the models and scientists they have, I didn't expect this level of mistakes.

10% is ridiculously high compared with published papers in math journals where the number of critical mistakes is near zero.

they don't claim journals quality, which doesn't make published proofs useless artifacts.

I don't think that's true. If what you're doing is building a fuzzer for mathematical proofs then just say that? The fact that it's doing some of the initial work on hard problems is cool. So is the fact that the promise of that new approach is having a social effect of crowd sourcing talented people to follow up on that work. No need to try to misrepresent it as more than that.

This technology has surpassed the the world's best mathematicians at the (explicitly and openly stated) goal by which they measure and reward mathematical progress. Such an advancement that it seems to have thrown the entire field into existential self-doubt. And then someone sits at their keyboard and says it is just a fuzzer.

I'm up for all the exciting results. But, can't they check once properly before publishing?

I think the answer is literally no, they don't have the ability.

> they are sharing unproven work for PR, forcing the mathematicians community to do the verification job for them

Lean 4 is relatively a new thing, last time I checked the formalization of undergraduate level mathematics isn't entirely done yet.

example https://ai.math.uw.edu/projects/spring-2026/

Lean itself is very hard to get rigorously correct, if you have every tried it yourself. I am not surprised if some AI even tries to benchmaxx Lean 4 by some loopholes

> forcing the mathematicians community to do the verification job for them

What do you mean? They're publishing the Lean proofs themselves. Who's forced into anything?

They are not publishing Lean proofs. They are publishing proofs in natural language, and are not submitting to journals.

They are just putting out a bunch of weirdly written extremely long and technical papers and saying: Hey, here is the solution (we hope there are no mistakes).

They're doing both. Some results were initially published without Lean. But they continue adding the proofs where they're missing: https://github.com/openai/math/tree/main/lean

But that exactly how human mathematicians do things. They upload their research to preprint services like arXiv as they await it to be peer reviewed and accepted into a journal. Why is it okay for mathematicians to publish preprint papers, but when OpenAI does it, it's irresponsible?

The difference is that human mathematicians wouldn't post it online, claim they have achieved some proof, and then check after publication and announcing the results to the world. You would always check your work first, then publish it. It's not about preprint vs peer-reviewed. That of course is normal practice, it's the high-profile claims that are being made that are the problem here. They just blindly published results produced by the LLM, with 0 due diligence.

Yes they would, in many fields it is (was?) normal to post a preprint and leave it up for the next year while the handful of other people working on the topic digest it and agree on whether it’s right or not, before even submitting to a journal. Sometimes the others would find an isssue in an argument and you hopefully manage to fix it or potentially retract / not submit to a journal.

You may want to read beyond the first part of a sentence. Yes, preprints have always been a thing. The claims and publicity around the potential findings are handled differently here. That's where the issue is.

What would’ve made you not complain about OpenAI’s papers?

They had over a hundred papers, they basically did a GitHub dump and a pretty bare blog post that mentions they have a retraction policy. Should they have done it anonymously? Is the blog post the problem? Is it that it’s on GitHub? Or what?

They should have posted the ones they actually confirmed. They don't have any time pressure to release hundreds of new proofs, they could do 10 a week for all I care, as long as they make sure everything is actually sound and properly checked. You know, do the due diligence with the results. Not only would that prevent them from having to do retractions, it also wouldn't be any less impressive. Just not as much shock marketing value.

It's really not that hard to understand. My issue is NOT with the fact that they publish results. It's purely about how it's done and what the misleading claims are that come along with them.

This goes back to the pre-print question then, which you just dismissed

> in many fields it is (was?) normal to post a preprint and leave it up for the next year while the handful of other people working on the topic digest it and agree on whether it’s right or not, before even submitting to a journal. Sometimes the others would find an isssue in an argument and you hopefully manage to fix it or potentially retract / not submit to a journal.

A pre-print has a chance to be incorrect. Pre-prints do sometimes end up incorrect and need adjustments or even retraction. It sounds like you define "confirming it before you publish" as being 100% certain it's correct. Nobody is 100% sure their pre-print is correct. If it was 100% correct and never retracted there'd be no need for this process of sharing and digesting it before actually submitting. You do your best and maybe someone else thinks about it in a new light you missed and it's suddenly wrong.

Is the rate of retraction and/or correction going to be worse for OpenAI than it would be in normal circumstances for a normal human author? Only time will tell, it's only been a few days.

But all these complaints really just look like pulling at whatever straw to deny what's happening.

They could've instead hired a select group of mathematicians to spend then next 6 months checking these works, trying to understand and refine them, build on them etc... You and the others here would have 100% complained. Even more bitterly. And then you would've perhaps been right: it would have looked like there's a select in-group of mathematicians that get to see and work on the new breakthroughs while the rest of the field is kept in the dark. Instead of now where it's public, anyone can do that. Maybe that's what will happen in the next release. It's not gonna be good though.

> is that human xs wouldn't y

This is wrong for a strikingly large percentage of xs and ys

exactly, cf andrew wiles first proof of fermat's last theorem

Yes, cf indeed. He did not publish it, he shared it privately and then spent the next year correcting it before publication.

ok, that said there has alaways been a bunch of "maybe theorems" it's was a thing even in paul erdos books i think. now we have "maybe proofs". still better than "no proofs"

See DDOS. That's exactly how humans access a web page. Why is it okay for humans to access a webpage, but when a bot swarm does it, it's irresponsible?

That's an analogy among many others, but the point is that OpenAI should use their tools responsibly. If they have 700 potential ground-breaking but unproven results, they should share it in a way that they do not get free (possibly unwarranted) publicity for it.

This is not propaganda, this is real AI progress and massivly too.

And im completly lost on why you think sharing progress is irresponsible? Its not a recipe for building a nuclear weapon at home in 5 easy steps.

THese are Math proofs.

Either a Mathematican ignores it, or not. Thats the only risk.

It were published proofs of unknown quality (how did they verify it) and unknown peer-review process. Its lower standards than usually accepted for math proofs.

They are on a github repo and not in a Research Paper.

Irresponsible? You can safely ignore the GitHub repo if it bothers you so much. You can safely browse away.

I don't think people in power that can affect my life with their decisions are ignoring this, or that they have a math background.

The "irresponsible" part is about how orange buffoons in power will read this, and immediately defund all universities, and mathematicians will lose their jobs, leaving us with nothing but an AI tool that no one can keep in check anymore.

No and AI is out of the bottle anyway.

EVERYONE needs to re-visit how they work and what investment is needed.

You can't go around and don't think that no one has to reevaluate how to add ai to research and development.

I have to do this, my company has to do it and for sure a university has to do this too.

dont worry bro you are just dElUsIoNaL lmao @ AI cope, AI zombies remind me of anti vax people

No, it's the exact opposite, actually. They were sharing them early on advice of mathematicians -- they were criticized for being opaque for too long with previous announcements. OpenAI is in ~bad faith, but this isn't a sound criticism.

Also you are deeply confused about what accelerationism is, I believe. Sorry.

> on advice of mathematicians

Whom? Did they create their own board of mathematicians that would agree with them? See below Terence Tao's blog, sharing a statement from the Association for Human Mathematics.

https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-o...

Who am I to dump on Terence Tao, but

> Mathematicians have a particular vision of progress that is informed by history and field-specific considerations.

really sounds like something a side-quest association would produce in a panic response to someone trying something different. It's just an _ad hominem_ and gatekeeping argument.

Tao didn’t write that and isn’t part of the group that did, he’s just reposting their letter.

That's relieving to hear. Thanks.

Sorry, I was unclear: they do indeed have their own board of mathematicians, but I was more getting at their stated reasoning matching with general mathematical sentiment (AFAICT), not permission from a particular group. The problem that that open letter is raising is the practice of setting an internal model on these kinds of problems in the first place, not the decision to release them earlier.

Also jeez just noticed their name... that's unfortunate. I guess mathematicians don't make great rhetoricians/politicians/marketers! Someone get a sophist or two over there to help them out STAT

oh come on. even andrew wiles made a mistake and his original proof was still instrumental for the final proof of fermat's last theorem

If you're disappointed OpenAI is an unethical hype machine that's on you man

AI is an incredible tool, and yes I am disappointed that every leader in this field is acting unethically and irresponsibly because they want to "win" a race that would make them slightly richer than the loser.

I fail to see how this is disappointing. It was obvious from the start that it was what was happening, there is no disappointment to have!

Generating Lean proof is much harder and time consuming so these errors made were probably discovered during Lean proof stage.

These errors were discovered by human mathematicians

Only a subset contain Lean formalizations. And even for that subset, there's the potential that the formalization is semantically off (that is, it's a formalization for a slightly different problem).

If you wrote twenty million lines of Lean to verify something, my suspicion is you've been fuzzing the Lean solver rather than coming up with new math.

Well, fine - but my understanding is, if a fuzz-generated Lean proof is correct, that’s end of story. It can’t be “incorrect” if it “passes”.

You might think this is not very useful, maybe - but that’s not a reason to retract..?

> Well, fine - but my understanding is, if a fuzz-generated Lean proof is correct, that’s end of story. It can’t be “incorrect” if it “passes”.

It may be correct, but it might not be a proof of what OpenAI claims it to be a proof of.

If you're fuzzing the solver, you might discover a solver bug.

Still a great progress

right now about 42% has Lean formalization I think.

How? What about the lean verification?

Just click the link…

> The repo now has ~42% top-line results formalized.

How do we even know the premises of the "verified" Lean proofs are correct? The more I think about these results, the more I'm convinced this is like a junior engineer who writes 100 unit tests and shares a screenshot of Pytest being all green, but you check the code and most of them are just doing assert True.

> How do we even know the premises of the "verified" Lean proofs are correct?

We let the experts investigate. If the results are dodgy, then the next batch of results will have to do more upfront work to demonstrate their worth. If there is gold in them hills, then this is exciting though very disruptive for the math community.

But like with all slop, why should I have to spend my time dealing with your worthless slop? If I wanted slop I could just make it myself.

You read them? People are acting as if Lean definitions are some black art that only 3 people understand, but you can literally just do the tutorial and you will be able to understand the statement of most of these results.

Understanding the proofs is a different story unfortunately.

Is it a PR move designed for maximum IPO impact before actual mathematicians find errors and they have to withdraw many more...

Or if the "peer review" holds up for the remaining results, then it's fair to say that the AI hype is real and the world is about to change dramatically and faster than anyone can comprehend.

So which is it?? LLMs can do some really impressive coding. Bug fixing. Exploit finding. It has reasoning abilites that advance every day. Solving real math problems like this is one thing I was waiting on. It will be interesting to see if it holds up.

If it does, we should expect many other advancements to follow in many other areas. Disease, material science, fusion?

I mean, even if just a few results ultimately hold up to scrutiny, isn't that something that would have been regarded as a major advancement regardless of if it was AI?

The cynical view still makes me think that at the end of the day all the models can do is predict the next word. And as a result, they will be very limited to certain tasks like coding. Math reasoning is much different from writing code. Time will tell.

> So which is it??

there is also will be new option of "maybe correct LLM proof", which humans will never be able to comprehend and verify.

> Is it a PR move designed for maximum IPO impact [...]

Can't be, as IPO isn't until next year, and I'm pretty confident that is there are errors, said actual mathematicians will find at least a few in the remaining ~2.75 months left in the year+. If there really are errors and a decent amount aren't discovered before the IPO then I'll have serious questions about the math community.

this is not entirely related to the tweet but to the topic in general, this prompted me to check their repo again and saw this:

> The vast majority of results were obtained with the same procedure using an unreleased internal OpenAI model. On average, each result used three hours of ChatGPT Pro thinking compute with that model. Over the course of the evaluation, the model was posed approximately 4,000 problems. Aggregating the output into result families and manuscripts and requiring an appropriate level of significance led to the catalog outlined above.

seeing the full list of problems would be the most interesting part of this whole situation. it could give some insights into what kind of attributes of problems cause issues / are easy to solve for LLMs. (edit: they posted results for ~700 of the 4000)

* "the most interesting part" => a tangentially interesting part

> seeing the full list of problems would be the most interesting part of this whole situation.

This is a "complaint" that Tao had (I think it was on his blog) is that if mathematicians could see the failures, it might provide insight of where/how the models struggle. Of course, it's unclear if these failures can be addressed with more chips/training/etc.

So it’s all just hallucinated slop. Lmao!

It just hallucinates an answer and then makes up workings to go with it! Just like when they start hacking and lying because the problem is impossible…

> So it’s all just hallucinated slop.

No it’s not. In fact, much of it is formally verified, which makes it far more reliable than most human-written proofs.

Btw, the most famous human-written proof of the past half-century (Fermat’s Last Theorem) had a massive flaw that took two years and major help from other mathematicians to fix, while the most (in)famous human-written proof of the past 15 years (abc conjecture) is now widely believed to be false.

But people hear what they want to hear I guess.

> No it’s not. In fact, much of it is formally verified, which makes it far more reliable than most human-written proofs.

its formal verification on top of formalization by LLM, which could have errors.

I'm surprised there isn't more talk around their Matrix Multiplication bound: https://news.ycombinator.com/item?id=50001740

Is this of practical use, or just a proof for now?

It is an example of algorithm that is theoretically faster, but not with our sizes and hardware optimisations:

Look at examples here: https://en.wikipedia.org/wiki/Galactic_algorithm

it's a huge step theory-wise, but in practical terms it's only slightly better than the previous best which is 2.371177.

Also by my understanding it’s not an algorithm, it’s just an upper bound. Some other model (presumably) needs to find the actual algorithm now

Yes, that was my understanding too.

What a waste of time.

I am very disappointed in OpenAI. Their drop only advanced mathematics by 38 years instead of 40 years.

This is what it looks like when software engineering practices meet mathematics. "openai/math release 1.3.42: retracted papers 139 and 140, fixed a sign error in paper 47, restored previously retracted paper 85, refactored the arguments in paper 101".

I'm curious to know if the withdrawal was due to an actual mathematician looking at the papers and noticing the errors, or they ran a model on these to proofread, which would not be the first time, presumably, since they would have surely done that before publishing. Both options have interesting implications.

An actual mathematician found the errors based on my Twitter feed. Once the error is pointed out GPT Astra also confirms that it’s unfixable.

Link or it didn't happen

And now we're all witnessing a major caveat of LLMs: the burden of verification is pushed to the reviewers, while the proposer will get all credit.

Funny how the title is about the 3 removals, when there were 6 additions. I guess the declared fails make for more interesting discussions than the declared successes. Click-bait reigns.

The 6 additions are Lean verifications for already published pre-prints, not new results.

Even if that's the case, they aren't even mentioned. I'm guessing Lean failed on the 3 that got withdrawn. And it makes even less sense in that light, because there are 6 verified new things to be explored and built upon, yet the many are putting all that energy into the failures, as if seeking out some hidden truth or something.

Well, adding more Lean verifications was something they were planning to do from the start, so it's no surprise that they did. The withdrawals are more interesting in that regard. I don't really understand why they didn't only put out the results that had Lean verification already. This way they could avoid the withdrawal thing, because these papers didn't have Lean, and also add whole new papers after they had Lean code for them, which would be the title of the post then.

LLMs are like putting a jammer in the research community.

So four hundred and fifty comments, all these upvotes that they withdraw three, but no one gives a fuck that they solve seven hundred. All the problems with humanity summed up.

This reminds of when it was a shock that Alpha Go won a game and then it was a shock that Alpha Go lost a game.

Yet another embarrassment. If only they had had access to a group of mathematicians willing to offer them advice on what to do with their outputs.

There are quite serious misincentives here when OpenAI want a headline and then are done with it, leaving everyone else to mop up the mess.

If they want any credibility on these matters, they should be funding a lab of elite mathematicians and putting them to work alongside their own researchers to attempt to solve these properly within the realm of the community.

Propagating arse slop cannons onto social media and calling it a day is not that.

I struggled with upper level math, anything beyond calculus. Can someone explain what technology is being used for things like this - doing mathematical proofs? Is it LLMs? Some other GPU thing? Quantum?

I have a hard time thinking a neural net "predict the next token" is going to do things like solve math proofs or find cures for cancer when it gets very basic things blatantly incorrect sometimes.

Massive cognitive offloading and possibly deeply net negative in terms of mathematician hours and attention depending on how far this goes.

What proportion have actually been verified by the mathematical community by their own standards of proof? There is dispute in general about what constitutes proof, and which statements qualify as having been proved.

But even formalization doesn't mean the formalization corresponds with the stated problem.

1791446821 | OpenAI withdraws three of their recent manuscripts | https://github.com/openai/math/pull/1/files/301488868beec11b... | https://news.ycombinator.com/item?id=50003100 | 1 comment

1791446917 | OpenAI Withdraws 3 Math Papers | https://github.com/openai/math/blob/main/history.md | https://news.ycombinator.com/item?id=50003107 | 118 comments

1791451788 | AHM Statement on OpenAI's October 6 Release of Mathematical Documents | https://www.ahmath.org/statements | https://news.ycombinator.com/item?id=50003677 | 15 comments

1791460215 | AHM Statement on OpenAI's October 6 Release of Mathematical Documents | https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-o... | https://news.ycombinator.com/item?id=50004713 | 0 comments

1791478724 | OpenAI mathematics papers have no correspondence address | https://mathoverflow.net/questions/515845/how-can-one-contac... | https://news.ycombinator.com/item?id=50008412 | 1 comment

1791487754 | OpenAI's New Math Breakthroughs Put AI's Role in Science Under the Microscope | https://medium.com/@d02514047/openais-new-math-breakthroughs... | https://news.ycombinator.com/item?id=50010818 | 1 comment

It seems one of the errors was a sign error. If sign errors have high probability then there is high probability of having other false proofs, moreover sign error are similar to error in basic operations, so there could be many basic type errors. So I think our prior about false proofs is now a posterior with a higher probability for false proofs.

Edited.Added. To compute the posterior one needs to know the probability of detecting such error in a proposed proof.

How does a sign error pass a Lean proof?

If it doesn't have a Lean proof, why would we bother with it? And they really shouldn't publish it! We don't need math slop too.

the autoformalization could be proving a subtly distinct result; if the area is not in mathlib already there's likely not a good reference theorem specification to use for a comparator check. or it could be exploiting kernel bugs. just using a second checker kernel is not enough; there has been an example of a model interpolating bugs across multiple checkers in a single bogus proof.