Overview
- OpenAI announced that an internal, unreleased AI model produced a proof showing a smooth, stationary fluid can develop a finite‑time singularity under smooth external forcing and that GPT‑6 Astra completed a Lean formal verification of the argument.
- The company reported the proof was generated by roughly 10,000 cooperating AI agents working about 88 hours and that the formalization step took about 17 hours, with outside estimates putting the compute cost in the tens of millions of dollars.
- Researchers Tristan Buckmaster and Levent Alpöge, who published related fluid‑equation work, have asked whether OpenAI shifted resources after learning of their progress and whether material stored in OpenAI’s Codex influenced the result.
- OpenAI denied targeted access to specific user data while acknowledging it cannot rule out that anonymized product data helped improve its models, and the company said it will not seek the Clay Mathematics Institute prize for this claim.
- Mathematicians praised the technical ambition but stressed that formal verification does not replace peer review, independent human checks are ongoing, and the episode raises questions about credit, data use, and the role of large, well‑funded labs in pure math.