I don't think the claim is "they definitely have an oracle that solves the problem, and I reject it because it's hard to read". The claim is "OpenAI claims to have used an oracle to solve the problem. The proof is very difficult to read, and to even know if it does or not, we have to go through it with a fine-toothed comb, but they're going around claiming they definitely solved the problem (or at least getting press that claims that which they aren't pushing back against) and this might convince the people who sign grants even if it isn't true"

People who are invested in the idea that we've invented a general intelligence, now, which includes all these companies that are literally financially invested in this claim they are making, will tend to believe that its results can already be trusted in domains like this. Some mathematicians seem to believe some of the proofs written by their models, and some, like this one, don't. I do think it's valid for an expert to push back against the claim that the best use of their time right now is to verify the poorly written work of everyone who's claimed to solve the problem

Over the year, nothing they've released with a lean proof attached has turned out false (That's sort of the entire point. It's not impossible but it's really difficult). There's a reason most mathematicians, including the ones vehemently against OpenAI's dumping are not arguing the results are secretly false or have a high potential to be. And indeed, if that were the case, it would quickly become apparent and all this worry about grant signers would vanish into the wind. It's very easy to ignore nonsense. The problem is that it isn't nonsense.

I really don't know enough about it to know whether you're right or not, nor do I know whether or not you know enough to make the claim you're making, so I won't make an argument one way or another because it's non-sequitur to what I said anyway. The fact that you or I or Sam Altman or Terrence Tao believe the claim is irrelevant to whether this obligates the person who wrote the blog post to believe the claim, and it sounds like he's willing to consider the possibility that it is right, and would read the paper if it reached a threshold of comprehensibility expected of people making that kind of claim.

I's not a non sequitor because it cuts right to the point. He's under no obligation to read it sure, but that doesn't mean Open AI isn't justified in claiming to have proved it. The justification isn't Sam Altman's belief or Tao's or anyone else's authority. Results accompanied with lean-verified proofs whose formal statements match the problem at hand have arguably stronger justification than the vast majority of human math publications.

> Over the year, nothing they've released with a lean proof attached has turned out false

That's not true. [0]

> On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types.

Even in this dump we're talking about, it hasn't been true. [1]

> In “Algebraicity of Weil classes on split abelian eightfolds” a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.

[0] https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

[1] https://github.com/openai/math/blob/main/history.md

1. That wasn't from Open AI or any major lab. I don't know what random people are getting to. It's curious also that it had no natural language proof attached. Usually these labs have a NL proof then translate to lean. Lot less possibility of lean maxxing.

2. None of the results Open AI retracted had an attached lean proof

I don't understand. Why is this the onus of scientists and PhDs to review whatever results OpenAI had dumped out? If OpenAI had produced incomprehensible papers, surely any journals would just reject it, or demand the author to do a complete rewrite? Unless we are talking about a race to solve problems, which PhDs are afraid that they had been scooped up on?

The problem isn't just that the papers aren't fun to read. The problem is that a lot of the research that goes into solving these issues leads to other discovers, new fields to explore and people have to develop new approaches to solve them. The other part of it is, the quality and the enjoyment of working on these problems leads people to find new and other interest problems to work on.

If you just strip mine the answers and Sam Altmans magic button solves 100/100 problems, what's next? Who is left to come up with a new interesting question for the magic button to solve?

Lastly, life and the present moment is all there is, if there is no enjoyment in anything we do, then what's the point of all the "living for ever" Altman et al want to achieve.

We will live forever to read boring papers generated by LLMs? Literally sounds like an eternal hell.

People are already finding stuff in the release to get excited about, and as the models get better at distilling proofs to make them more coherent, this will only amplify. Of all the things to worry about, human curiosity and the ability to run with new ideas probably aren't at stake.

In fact, I can't remember a time when I was more excited about the future of science. This could herald an end to the replication crisis, and kill off bullshit science completely. The danger of course is that we end up with two companies effectively dominating cutting edge research in every field, but it remains to be seen if that's even possible given the pace of improvement in open weight models.

Nuclear fusion is already proven by the universe to be a viable energy source by the fact that the sun exists but people still work on understanding and taking it and developing new approaches to accomplish it. People didn't stop experimenting with and developing programming languages because technically they're all turning complete and the first one was "enough." Y'all will be fine - every JavaScript framework that exists is someone looking at a theoretically correct and complete solution and deciding actually it sucks and they could do better. "I want to understand xyz but the proof is trash and I think it's ugly" will be plenty motivation for a lot of people to work on it.

How is the journey to understand fusion related to not wanting to spent your limited time on earth wading through AI slop?

You don't have to wade through the slop. The point is a giant star in the sky figured it out and that doesn't demotivate you from figuring it out yourself

Here's a guy who's made a "beyond n log n" tracker: https://x.com/aurel_pr/status/2108214135179944096

He's tracking the community progress on sub-n log n multiplication. OpenAI started with 1 - 1.63e-55. The result has been now improved on 115 times, and the current record is "rohanarun"'s 1 - 9.87e-5. I'm sure by tomorrow it'll have improved again.

Does this look like people aren't having fun? Does it look like they aren't discovering stuff? It looks like it's spurred a cascade of interesting community activity. It doesn't really seem much different from what happened with the twin primes conjecture. Isn't that supposed to be the point of all this?

Some people are having fun doesn't negate the rest of the issues with this sort of thing.

then the rest of them can pound sand.

It won't be like that, it will just divide the scientific community. The vibers and the people who do the work.

I see it in my job now, there are people who do the work and know what's going on, the people who actual get shit done. Then there are the people who just leach of everyone else, vibe and have a bunch of prototypes adding no real value.