OpenAI releases ~700 maths manuscripts; its Navier–Stokes proof is soon questioned
- WHAT HAPPENED
- On 6 October OpenAI published results on open maths problems from an internal frontier model, with Lean formalisations and details on GitHub. Commentators count about 722 manuscripts but differ on how many major problems were solved. On 8 October New Scientist reported that the human-readable and machine-checked versions of its Navier–Stokes proof do not match.
- WHY IT MATTERS
- It is the largest single AI maths release yet, and it shows formal verification can itself be mistranslated—raising the question of how to review AI output at volume.
- WHO IT AFFECTS
- Mathematicians and theoretical computer scientists, journals and reviewers, and the formal-proof community.
ORIGINAL SOURCES
OpenAI News · Sharing AI progress in mathematicsNew Scientist Tech · OpenAI mistranslated mathematics into code for its Navier-Stokes proof