Cambridge/King’s College researchers argue Lean verification of AI autoformalization does not guarantee faithful translation of natural-language proofs. SCI hierarchy argument: resolving NL ambiguities for faithful translation is formally harder than the Halting problem.
OpenAI Navier–Stokes case (Example 3.1): Lemma 8.6 equation (8.19) in the NL paper bounds torus derivatives with m+4 input derivatives; cited Lean at commit f9e8bc5 uses m+5, yielding a weaker estimate. NL proof cites (1+|k|)^{-3} summability; Lean path uses Fourier-series machinery with exponent 4 in places.
Paper does not refute OpenAI's mathematical claim — only that the Lean artifact is not a faithful formalization of the NL proof as marketed.
OpenAI told New Scientist it is aware of mismatches and will correct NL errors as found while continuing formalization work.