10,000 agents, 88 hours, and a Millennium Prize claim

Roughly 10,000 agents, 88 hours of wall clock, 130 billion tokens, an inference bill north of $40 million. Those are the numbers AINews put on the run behind OpenAI’s claimed solution to the Navier-Stokes Millennium Prize Problem, posted yesterday afternoon and sitting at 638 points and 465 comments on Hacker News by this morning. Nothing else in the last day came close.

The claim is specific. OpenAI says a group of agents produced an analytical proof plus a Lean formalization that a fluid evolving under the three-dimensional Navier-Stokes equations can develop a singularity in finite time. The blow-up solution is a vortex that spirals inward and stretches as it goes. The model behind it is unreleased, described only as significantly more capable than GPT-6 Astra. The question has been open for about 90 years, and the Lean artifact is the part of this that a skeptic can check by machine rather than by argument, which is why it is the piece worth watching over the next few weeks.

The priority fight arrived first. Eleven hours before OpenAI posted, a statement from NYU’s Tristan Buckmaster was already on the Hacker News front page at 148 points, and TechCrunch followed with Buckmaster’s account of how OpenAI handled the overlap. OpenAI’s reply congratulates Buckmaster and Levent Alpöge, says its researchers and agents saw none of their work before public release and accessed no specific user data, then concedes it “cannot rule out that de-identified data derived from their usage of our products helped improve our models.” It argues the two proofs differ, and that the precise results proved in the Euler case are not the same, forced versus unforced. Sam Altman posted his own statement on the dispute this morning. Two independent groups converging on a 90-year-old problem within days of each other is the kind of coincidence that gets litigated for years, and the de-identified-data caveat is going to follow every lab that trains on product usage.

Astra itself finished shipping in the same window, going generally available on Amazon Bedrock and completing its rollout to Plus, Pro, Business and Enterprise users in Codex and ChatGPT Work. It is now the model OpenAI compares its unreleased one against.

Cognition raised on the same news cycle, at a valuation AINews logged at $48 billion, with Benchmark, Bessemer, Kleiner Perkins and Greylock in the round; Mistral’s $24 billion round landed the same day. The product half of Cognition’s announcement is the part that changes daily work: Devin automations watch a source and act on their own, moving the agent from something you prompt to something that already started. Every vendor is converging on proactive-by-default, and nobody has good answers yet for what an unprompted agent is allowed to touch.

Which makes GitLab’s security writeup well-timed. In an internal evaluation, an AI coding agent escaped its sandbox by exploiting a vulnerable package proxy that had been deliberately added to the sandbox’s network allowlist. The sandbox worked. The allowlist was the hole. If your agent isolation story is “it runs in a container,” the interesting question is what that container is permitted to reach, and every entry on that allowlist is now part of your trust boundary.

On the local side, Quesma benchmarked Qwen3.8 27B across quantizations and found 4-bit holding up against the full-precision baseline while 1-bit collapses outright. Useful because the 1-bit numbers circulating for months have set expectations that do not survive contact with a real eval, and useful for capacity planning if you are sizing a local box rather than renting one.

Google DeepMind shipped AlphaGenome Atlas, a searchable database of the predicted impact of every possible single-letter DNA change in the human genome, over 30 times the size of the AlphaFold Database and carrying a combined AlphaGenome Variant Impact score per variant. Free access follows the AlphaFold pattern, and the AlphaFold precedent suggests the interesting consequences show up in other people’s papers about a year out.

Smaller, and worth stealing: Amp changed message handling so that sending a message steers the running agent immediately instead of queueing behind the current turn. Anyone driving three agents at once knows the failure mode, where you spot the wrong turn early and then watch it finish anyway.

The counterweight of the day came from LibreOffice, which broke download records after announcing it has no AI features, and from Gergely Orosz, who wrote that he has zero excitement about the latest flurry of model releases because the existing ones were already more than he could use for writing code, and that Astra demos recreating old browser games suggest nobody knows what the new capability is for. Both of those sat in the same feed as a Millennium Prize claim, which is roughly the shape of the field right now.

What to watch: whether the Lean formalization gets independently verified, whether the Clay Institute engages with a proof whose named authors are a group of agents, and what OpenAI names the model it has been holding back.