Mathematicians identify mismatch in OpenAI's Navier-Stokes proof versions

A team of mathematicians claims OpenAI's written Navier-Stokes proof and its computer-checkable Lean version differ, New Scientist reported. OpenAI acknowledged the mismatch and said it does not mean either proof is invalid. The researchers identified a condition in Lemma 8.6 that requires a value below m + 4 in the written proof but below m + 5 in Lean, a weaker requirement. Lean lets computers check logical statements, but checking one version does not establish the correctness of the other. The team took about two weeks to identify the discrepancy, compared with the 88 hours OpenAI said its agents spent generating the proofs. The researchers have not concluded whether the written proof is correct.