OpenAI's Navier-Stokes proof has a hidden code mismatch
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
OpenAI's surprise solution to the Navier-Stokes problem came in two versions: one for humans and one for computers. Mathematicians say the two don't match, revealing a subtle translation error. The proof itself may still be correct, but the discrepancy raises doubts about whether AI-generated mathematical results can be trusted without human review.
What has to be done with all of these large language model-generated proofs is that they will have to be read by humans, and this creates an enormous extra burden on mathematicians.
- krackers
- jey
This headline is completely wrong. The proper coding analogy is more like, the natural-language paper was the "design document" before coding it up, then when coding it up as Lean4 proofs, specific details were realized to be slightly off[1] and corrected while writing the implementation in code as machine-checkable proofs. Which I'm sure is an extremely relatable situation for most of us here. But the paper or "design document" wasn't corrected afterwards.
I also think this "paper then code" approach is now obsolete. The modern way, in AI-assisted workflows, is to first iterate on "derivation sketch <-> machine-checkable proof" incrementally building out your result. You can of course leave `sorry` placeholders along the way and fill them in, so it's not like you're restricted to going entirely bottom-up. Finally, once you have a `sorry`-free proof of your top-level statements (theorems) of interest, you can then work on writing up the exposition in LaTeX based on the lean code.
1. See https://arxiv.org/abs/2610.08144 for details, but an example they point out is that a key bound required 5 additional orders of derivatives (and stated in Lean that way), but the paper claimed that the bound held with only four more derivatives.