Dr. Pierre Thibeault

BREAKING: OpenAI’s solution to Navier–Stokes does not match its Lean verification. The most important article to read today is not one of OpenAI’s 700 AI-generated math papers. It is this other paper, making a deep and worrying point: A Lean-verified proof does not automatically validate the proof written in natural language, nor does it mean that the formal statement captures the intended theorem. During translation, an AI can change an assumption, weaken a statement, or replace the argument entirely. It can hallucinate another theorem. Lean correctly verifies the result. But the proved result may no longer be what the paper claims. This is a general problem. Things get spicy when the authors examine OpenAI’s proposed Navier–Stokes solution. They identify at least two mismatches between the written intermediate results and their Lean counterparts: One estimate claims that four additional input derivatives suffice. The Lean version requires five: a weaker result. A pressure-flux estimate is obtained through a different bound, and proved through a different argument. It is not clear whether these mismatches invalidate the entire proof. But they raise an important issue. OpenAI is flooding us with claimed revolutionary breakthroughs. Yet nobody knows whether the proofs are correct or whether they prove what they claim to be proving. Epistemia at scale. * Paper in the first reply