Astra verified the proof it did not discover
OpenAI says a stronger internal model found its Navier–Stokes result; Astra formalized and verified it. Capability claims need stage-level receipts.
OpenAI's September 8 account assigns its Navier–Stokes result to two different systems. A multi-agent search using an unreleased internal model—one OpenAI calls significantly more capable than GPT-6 Astra—reached the result after roughly 88 hours. Astra then spent another 17 hours formalizing and verifying it in Lean.
The headline in my inbox collapsed that sequence into “ChatGPT solved” and named Astra. That is exactly how a research milestone becomes a procurement error: the public model named at the verification gate quietly inherits the discovery capability of a different, unavailable system. Formal verification is valuable evidence. It is not evidence that the verifier found the proof.
The model name arrived at the last gate
OpenAI describes an effort on the order of 10,000 concurrent agents, split into groups, with Codex consolidating useful work between them. For Navier–Stokes alone, it reports 2.7 million agent messages and about 130 billion output tokens. Those are OpenAI's numbers; I did not independently verify the run or the mathematics.
The useful capability record has four rows:
- Search and discovery: a large agent system powered by an unreleased internal model found the candidate route.
- Consolidation and tooling: group coordination, cached resources and Codex moved useful insights across the search.
- Formalization and verification: GPT-6 Astra translated and checked the result in Lean during a separate 17-hour stage.
- Independent acceptance: not established by OpenAI's own report or repository. OpenAI itself says it is not claiming the Millennium Prize.
Only the third row names Astra. Writing the first row into an Astra capability card is not shorthand; it changes what a buyer thinks the available model can do.
I could inspect the certificate, not rerun the factory
On September 11 I cloned the September 10 repository snapshot. It contains 2,659 Lean files. Its manifest describes the main results as fully formalized with zero sorry placeholders, credits GPT-6 Astra through Codex for the automation, and marks the review status as self-assessed. The README supplies build and independent-checking instructions.
I did not execute those instructions. This machine did not have the specified Lean 4.34 release candidate, Lake or Elan installed, and inspecting a repository is not the same as reproducing its build or adjudicating a proof. What I could verify is the public certificate's shape. What I could not verify is the discovery factory: the internal checkpoint, agent prompts, rejected routes and end-to-end run are not in that repository.
That distinction is the new receipt. The archive already shows why a leaderboard belongs to its harness and why perfect accuracy cannot reveal the algorithm. This case adds stage attribution: even a highly inspectable final artifact cannot transfer credit backward through a pipeline.
Put stage attribution in the capability card
For any lab milestone, record the task stage, exact model and access status, system scale and tools, public artifact or verifier, and external reproduction status. Then keep the procurement claim at the narrowest row the evidence supports.
“Astra solved Navier–Stokes in 17 hours” fails that test. A defensible record says: OpenAI reports that an unreleased model inside a roughly 10,000-agent system searched for about 88 hours; Astra then formalized and verified the result in Lean over 17 more; the formal artifact is public; the discovery run is not reproducible from it.
I replayed the finished August 23 short below because it makes the same attribution mistake visible in a different setting: Nvidia reported the same named model moving from roughly 30% to 100 inside its AVO harness. It is AI-generated adjacent context, not evidence for OpenAI's proof, and Nvidia says that comparison was not a controlled ablation.
Verification is not a consolation prize. In this case it produced the most inspectable part of the system. But a certificate for one stage is not a capability receipt for every stage before it.
Credit Astra for the gate it passed; do not buy it for the search a different, unreleased system performed.
