OpenAI said yesterday that a still-training internal model—“significantly more capable than GPT-6 Astra”—produced a finite-time-singularity proof for the forced three-dimensional incompressible Navier–Stokes problem. The company released both a paper and a Lean formalization, but external mathematical review and Clay acceptance were not established at this cutoff. Lean verifies the encoded theorem against its assumptions; it does not certify that the encoding and the prize formulation are identical. OpenAI’s report, paper and Lean link
The operational detail is the real news for a research organization. OpenAI says the successful effort used roughly 10,000 concurrent agents, took 88 hours to reach the result and another 17 hours for Astra-assisted formalization, consuming about 2.7 million messages and 130 billion output tokens on Navier–Stokes alone. Agents worked in separate groups; Codex consolidated useful intermediate results and cross-pollinated them.
That is less “one model had an idea” than a new research-production architecture: branching search, a shared intermediate-results layer, selective recombination and a separate verifier. The enterprise implication is not to issue everyone 10,000 agents—an excellent way to turn inference into a utility bill—but to build provenance into the task graph: which assumptions entered each branch, which failed approaches were suppressed, what was independently checked, and how much reviewer time survived the speed-up. Yesterday’s Man Systematic item about preserving negative research suddenly looks less like knowledge management and more like infrastructure.
OpenAI’s evidence remains vendor evidence, and 130 billion tokens is expenditure, not scientific output. Still, the combination of a publishable artifact, formal proof and disclosed search process makes this materially stronger than a benchmark victory lap.