OpenAI mistranslated mathematics into code for its Navier-Stokes proof (www.newscientist.com)

OpenAI's recent announcement claiming a solution to the Navier-Stokes problem has come under scrutiny due to a reported mistranslation in the formalization of its proofs. A team of mathematicians from the University of Cambridge highlighted that while OpenAI's natural language proof and its Lean code representation aim to convey the same results, they are inconsistent in critical aspects. For instance, an equation requiring a value to be below \( m + 4 \) in the natural language version changed to below \( m + 5 \) in the Lean version, resulting in a mathematically weaker statement. Although OpenAI maintains that neither proof is incorrect, this discrepancy raises concerns about the reliability of AI-generated mathematical results. The significance of this issue lies in the implications for the AI/ML community regarding the automation of mathematical proofs. As AI models like ChatGPT are utilized to auto-formalize complex proofs, the risk of unintentional alterations becoming undetected presents a troubling challenge. The Cambridge team emphasizes that human oversight remains essential in the verification process, suggesting that depending solely on AI for proof validation could lead to misunderstandings in mathematical results. This incident highlights an urgent need for robust techniques in auto-formalization to ensure the integrity of mathematical advancements powered by artificial intelligence.