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.
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?
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 make money off it.
> 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.
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.
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.
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.
> 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.
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.
> 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)
> 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.
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…
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. Both options have interesting implications.
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.
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.
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.
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.
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.
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.
63 comments
[ 5.8 ms ] story [ 74.0 ms ] threadIf that’s the case in a way its a similar delusion that average people are experiencing with their own AI use.
You could almost draw a comparison between that and inexperienced consultants making business changes, claiming glory and then disappearing before the thing falls apart.
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?
I vote for "automathon"
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 make money off it.
Or progress is not as straight forward in those fields as in math.
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.
> The repo now has ~42% top-line results formalized.
Understanding the proofs is a different story unfortunately.
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.
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.
there is also will be new option of "maybe correct LLM proof", which humans will never be able to comprehend and verify.
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.
> 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)
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.
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…
Is this of practical use, or just a proof for now?
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. Both options have interesting implications.
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 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.
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.
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
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.