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.
>>17070999I think we should start thinking of incomprehensible papers with Lean certs like strong numerical evidence. The level of inherent uncertainty is unacceptable to be anything more.
>>17070988The AI learned that if it added comments to every line that failed in Lean and replaced it with “0+1=1” then the errors would disappear and it would get a sweet green checkmark and more juicy tokens.The monkeys all clapped and smoked cigars when it happened. Even the women monkeys.
>>17070960Okay 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.
>>17071943>So what fucking difference does it makeThe difference between learning something and just burning open problems for the sake of AI corpo marketing.
>>17070960>entire mathematical community losing their shit over a machine that can produce an incomprehensible proof that's probably correct but virtually impossible to checkI thought "probably correct" was for empirical sciences, since when was this shit good enough for mathematicians?
>>17071943Which do you think is harder for an LLM: Correctly proving Quasi-RH or finding a subtle bug in Lean?
>>17072105surprised more people aren't saying thisLean is still a work in progressEven as recent as last month they were making bug fixes and "hardness" changes https://lean-lang.org/doc/reference/latest/releases/v4.34.0/#release-v4___34___0
>>17071947retard
>>17070960No one cares becuase the point was laugh at mathies. AI slop will be slop
>>17072105Both are halting problems
>>17072191>golem seethes impotently
>>17070988Both lean and natural language can be gibberish. It's like how LLM write compling code that does non sense
>>17071943>They still proved it whether you like it or not.The fact that the Lean proof check means the Lean proof is valid. It does not prove what they claim the NL proof (may or may not) show or be related to the NL proof in any way.>>17072727My code compiles!>but what does it do?It compiles!>exactly
>>17070960Yet the Jacobian conjecture is effing embarassing.
>>17071943The Lean proof proved *something*, but since it is inequivalent to the NL proof there is no guarantee that something has anyting to do with NS at all. It might as well just have generated a very complicated looking proof of 1+1=3-1 that is optimized to vaguely resemble a NS "proof" implemented in Lean.
>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
>>17071175>strong numerical evidence.weak numerical evidence more like. As long as you can write a 3TB diatribe of circular reasoning that ultimately compiles to 1+1=2 but *looks* like [important problem] at a glance, slop lean is less than useless.
>>17075276anyone with at least 2 working brain cells already figured out it's a fad. ai shilling is just the new schizo posting.
>>17077548Obviously, but they are getting annoying with their constant filter evading and rage baiting people into engaging with their slop.
>>17071943It tells you that there is an answer, but not necessarily that your prompting and the answer are connected properly. The AI could have found a different solution but just tells you that you're right because they're Yes Men by nature.
>>17075276>>17077550you guys STILL have not realized that 4chan as a whole is managed by shills? this website shilled for trump and the alt-right for years, shills for and spreads every single political/social campaign started by the paypal mafia (musk, thiel, ...). half the shit you see here is shady as fuck, and glows brighter than the fucking sun.
>>17080370I've been here for more than half my life now and I am still struggling to process the sheer levels of glownigger astro turfing on this site. You'd think a lot more people than just us would get at least.. mad at this? Where is the pushback?
>>17080405you get banned if you start a thread with some minor criticism, and even suggestion. meta threads are practically banned, even though gookmoot said 1 meta thread per board should be allowed.apparently rapeape and the other faggots managing this site have connections to glowies, politicians and maybe even the paypal mafia faggots... we don't control the site, and previous attempts at leaving en masse failed, so we're fucked.
>>17070960based in
>>17080405tried doing some pushback, got told my entire IP range was "banned for abuse". this site is like 90% glowniggers, agents of elite interests, intent on getting us to slowly walk into our extermination...
I love how no one actually read the article. The title is such a clickbait. It doesn't have anything to do with the Navier-Stokes problem; it just generally says that lean proofs can be wrong if the NL formulation is wrong. Even the first example looks more like a jailbreaking attempt than having anything to do with lean. They pose a statement (y = x^3 - x^2 - 1 + 1 when x > -1), which is true, then provide incorrect reasoning by swapping the multiplicity of -1 and 1, then ask it to provide a proof. Essentially, they are running an injection attack; they give it 90% correct information, then it expects in good faith that -1 and 1 are not swapped, so it takes it verbatim.
>>17081304low-IQ take>>17070999only intelligent post in the entire thread
>LLMs hallucinate and "cheat">people still fall for the FUD media campaignsquite sad to see.
>>17070960Shuddup luddite just trust OpenAI©®™ they have smart people who totally don't have financial incentive to falsify the result and IPO has absolutely NO bearing
I don't trust ANY source other than the furry intern at openAI.
>>17081413Consider that the alternative is employing billions of indians.
>>17082150no, it isn't. prove me wrong.
>>17082104Shut the fuck up, don't post shit like that here. Have some fucking shame.
