https://arxiv.org/pdf/2610.08144> To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean ‘verifications’. These include OpenAI’s announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.Has anyone on this board looked into OpenAI's proof? Or do we just trust them now?
>>17070960>does not guaranteeweak ass statement. not going to read the rest
Yes. I have looked into the 2026 OpenAI paper on the Navier-Stokes problem.UPDATE: still looking into it. I will keep you posted.UPDATE 2: Wow, I never expected this post to blow up!UPDATE 3: Since this post is getting so much karma, I just want to point out that OpenAI is operating on stolen land.
>>17070962>>17070964>we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equationsThe Lean proof and the NL proof don't match. Cope, AI shills.
>>17070960Which proof is wrong then?
>>17070970Potentially all of them.
>>17070976I meant between the NL and Lean language, but I have no idea what the difference is anyway. So maybe all of the other proofs are wrong too. But that's what the review process is for, right?
>>17070988Yeah or people could just ignore it
>>17070960No need to look into it. Look at how the mathematicians seethe about it. If it was nonsense they'd be saying so.
>>17070991Most people are just taking their word for it instead.
>>17070988Anon, you're not following. On one hand, you have an unverified natural language proof. On the other hand, you have mountains of humanly incomprehensible gibberish in Lean (effectively useless to a mathematician). Now it turns out there isn't necessarily any connection between the two. The reason """agentic AI""" needs proof checkers in the first place is to continually sanity-check its reasoning and keep it on track.What OP's paper implies is that the LLM manages to find a way around this, where it does whatever it wants in Lean while lying in the CoT, meaning there's nothing to stop it from hallucinating a bunch in the NL "proof" so long as the parallel Lean proof checks out. Maybe the NL proofs are still correct, but why would they be? The LLM isn't even relying on their correctness to produce the result.Effectively, you end up with AI slop and mountains of useless Lean no one can understand. Whether or not some of the NL proofs end up being correct, the approach as a whole is failing.
