The Unread Proof (www.poppastring.com)

OpenAI has announced a significant development in mathematical research by presenting a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof demonstrates that fluid dynamics can lead to a singularity (infinite velocity) when external energy is introduced, although it does not directly address the original question of whether fluid flow can spiral into infinite velocity on its own. To achieve this, OpenAI utilized roughly 10,000 agents, spending 88 hours on reasoning and 17 hours validating the result using Lean, a formal proof assistant, amounting to an estimated compute cost of $15 million to $22 million. The implications of this work are multifaceted for the AI/ML community. Firstly, the proof consists of 2.3 million lines of Lean code, which is so complex that even seasoned mathematicians find it beyond comprehension without AI assistance. This reflects a growing trend where developers rely on AI-generated code that meets testing criteria but may lack human understanding. While the financial investment and computational resources involved are impressive, the result serves as a reminder that sheer activity does not guarantee impact, as OpenAI's contribution addresses a different question than intended.