Overview
- OpenAI says an internal AI system produced a proposed finite‑time singularity solution to the three‑dimensional Navier–Stokes problem and released Lean formalization files to allow machine checking.
- The company reported using a massively parallel multi‑agent run that generated the proposal in roughly days and completed a Lean formalization in additional hours, claiming thousands of concurrent agents and billions of tokens were involved.
- Independent review is underway and the Clay Mathematics Institute has opened its standard prize review process but has not made any final determination about prize eligibility or credit.
- Mathematicians Tristan Buckmaster and Levent Alpöge had parallel unpublished progress and Buckmaster asked whether interactions with OpenAI’s Codex could have influenced the model; OpenAI has denied that those recent Codex prompts trained or were seen by the system.
- The episode has intensified calls across the field for new norms on verification, human‑level explanation, data‑use policies and authorship when AI produces formal but potentially opaque mathematical results.