OpenAI Lean Proof Mistranslation Exposes AI Verification Risk
Mathematicians at Cambridge have identified a mismatch between OpenAI's natural-language and Lean-formalised proofs of the Navier-Stokes problem, revealing that AI auto-formalisation can silently diverge from the intended argument to produce code that compiles but proves something different. The incident highlights a systemic reliability risk: LLMs tasked with formal verification may prioritise syntactic correctness over semantic fidelity, undermining trust in AI-generated outputs presented as verified. This is not a breach but a governance and integrity concern with broad implications for any high-stakes domain relying on LLM output verification.