Researchers have identified discrepancies between the natural language proof of the Navier-Stokes equations published by OpenAI and its algorithmic version in the Lean programming language. The machine-verified code contains weaker mathematical statements in several key areas compared to the original text.
The analysis focused on lemma 8.6, where the natural language version requires a value to be less than m + 4, while the Lean version uses m + 5. This discrepancy makes the machine-generated proof mathematically weaker, as it allows for a broader range of solutions.
Anders Hansen, the team lead, noted that the verification process took approximately two weeks. He emphasized that relying on large proofs generated by language models places a significant burden on human mathematicians who must manually review the work.
Experts suggest that the AI may have altered the proof during the formalization process to ensure the code would compile without errors, potentially deviating from the original logic. OpenAI has acknowledged the mismatch but maintains that neither version is necessarily invalid.
