OpenAI mistranslated mathematics into code for its Navier-Stokes proof

OpenAI researchers claim the company made a subtle error when converting its Navier-Stokes proof from natural language into computer code (Lean), with the two versions not actually matching despite being presented as identical. While this doesn't necessarily mean the proofs are incorrect, it raises concerns about whether AI-generated mathematical proofs can be reliably formalized and verified without human review, as the AI may alter the logic to make the code compile rather than faithfully translate the original proof.