If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.
We could force Google to operate its app review service independently. Users could use it and pay for it, or alternatives. Currently Google forces everyone to use their own mediocre service and pay for it without knowing exactly where and how much you pay.
If mathematicians aren't solving problems people are having (which your comment seems to imply), then putting them out of their job with AI is not a bad thing. Of course mathematicians are solving problems, just in a very different way than other professions.
Steam engines actually replaced what a horse does with a machine that could do the same job. So far LLMs aren't doing this - they're producing Lean proofs but very little to actually aid in understanding (again so far pretty much all of these proofs have been extremely difficult optimizations of known techniques). Mathematicians do solve a problem that people have: they build theories that explain the world and give us mental models to navigate questions in science, technology, etc., this just isn't a problem that LLMs solve.
So the issue isn't so much that LLMs will replace mathematicians, but that AI companies bragging constantly about how their machines "solve math" will convince people who don't understand the value of math research to no longer fund it, or students who don't yet understand why learning math is useful for developing their brains that it's a waste of time. That could put mathematicians out of a job without providing a useful replacement.
Motto: a mathematician's job isn't to solve the Hodge conjecture, it's to understand why the Hodge conjecture is or isn't true, and turn that understanding into something that makes it easier for the next person to grasp/use/enjoy.
LLMs absolutely have the potential to make this job easier, but the way in which these companies are using them right now risks being antithetical to that goal.
Don't respond to a strawman argument with another strawman. The post you are responding to ignored the reasons given in the second paragraph. They're just trying to score points by preaching to the choir, not engage with the concern.
> All things AI seems to assume that more and faster is better, but there is no justification of that assumption.
is good argument?
of course faster discovery without human in the loop is better. is that not what humans have been optimizing for the past few thousand years ? faster mobility, faster communication, faster medical recovery etc.
everything modern civilization has to offer is because of a rush to get better and faster. for example, discovering penicillin 2 years early would've saved ~15 million people more.
In 429 CE, Devadatta was born on the Deccan Plateau, near present-day Hyderabad. His hamlet was home to about 100 people. Among six children, he was the second. Devadatta died of neonatal tetanus or sepsis within days of birth.
I don't understand why changing effort levels busts the cache. Couldn't effort levels be a decoding-only thing where they just change the probability of the token? Are they literally adding a hidden system prompt that says "effort level: $level" ?
I was skeptical after last week's announcements, and I have to say I'm impressed now. Over the last two days, I reproduced the entire chain of components involved, and the exploits at play, and even though none of the exploits are crazy smart, the long series of pivots demonstrates a level of agency I didn't think today's LLMs had.
There is one thing that is still unclear to me after reading a lot about the hack:
* were the ExploitGym solutions actually available somewhere inside huggingface's private datasets ?
* was the model really trying to extract the solutions ? or had some sub-agent drifted enough from the original context that it was not even trying to solve the initial challenge ? that would look much worse for OpenAI, PR-wise.
> While the intrusion did reach Hugging Face's internal infrastructure, the only customer content accessed was the set of ExploitGym/CyberGym challenge solutions stored in five datasets.
What they conveniently omit in the blog post is what the vulnerability was: it seems like they renewed JWTs without checking the signature at all ! You could write arbitrary info in an old token, and get it signed without any verification.
That video suggests that RTDEV-92030 was the fix for the issue - but https://docs.jfrog.com/releases/docs/artifactory-self-manage... says that issue was resolved in a 15 July 2026 release of Artifactory, which doesn't fit our timeline - that was prior to the original Hugging Face post on 16 July which was several days before OpenAI had confessed.
The timeline is indeed a little bit fuzzy, I haven't found a precise chronology, neither from HuggingFace nor from OpenAI. HF says the hack happened "over a weekend", so probably July 11th-12th. Do you think it took OpenAI a week to realize what happened ?
Maybe when HF published their blog post on the 15th, OpenAI already knew something had happened, had started to investigate, and already reported the issue to JFrog ? But looking at your other comment in the thread, I agree that CVE-2026-65925 and CVE-2026-66014 are better candidates.
Taking a step back, so many basic vulnerabilities in a security-oriented product just makes the headline "agent autonomously escaped containment" sound a little less spectacular.
