OpenAI announced an unbounded counterexample to the Navier-Stokes existence and smoothness problem around September 8, 2026, reportedly accompanied by a Lean 4 formalized proof. However, it has yet to be verified by external mathematicians. Some commenters calculated that verifying a Lean proof of similar scale would take approximately 15 hours and 230GB of memory, while generating the corresponding code with an AI agent would require about 11 days. The estimated cost of this operation is around $40 million, equivalent to a human workload valued at approximately $132 million. Researchers Levent Alpöge and Tristan Buckmaster questioned the source of its training data, but OpenAI responded, stating that such a scenario is absolutely impossible.