to demonstrate the effect of this result we

A
Anonymous10/09/26, 08:46No.17070960
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?
op image
30

Replies

A
Anon10/09/26, 08:54No.17070962
>does not guarantee weak ass statement. not going to read the rest
A
Anon10/09/26, 08:55No.17070964
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.
A
Anon10/09/26, 09:00No.17070970
Which proof is wrong then?
A
Anon10/09/26, 09:47No.17070992
No need to look into it. Look at how the mathematicians seethe about it. If it was nonsense they'd be saying so.
A
Anon10/10/26, 17:51No.17071943
Okay the natural language proof is wrong. So what fucking difference does it make. The Lean proof is still correct assuming there is no bug in the Lean kernel. They still proved it whether you like it or not.
A
Anon10/10/26, 22:15No.17072104
>entire mathematical community losing their shit over a machine that can produce an incomprehensible proof that's probably correct but virtually impossible to check I thought "probably correct" was for empirical sciences, since when was this shit good enough for mathematicians?
A
Anon10/11/26, 19:13No.17072717
No one cares becuase the point was laugh at mathies. AI slop will be slop
A
Anon10/12/26, 19:56No.17073384
Yet the Jacobian conjecture is effing embarassing.
A
Anon10/15/26, 18:49No.17075276
>thread about OpenAnus doing anything (5 threads all bump limit) >thread about OpenAnus being exposed for lack of rigor (ignored+saged+hidden+called the cops) Maybe we should call them /sci/lls