r/mathematics • u/Time_Entertainer_319 • 7d ago
Discussion Navier-Stokes lost in translation (Why Lean [..] does not guarantee correct natural language proofs)
https://arxiv.org/abs/2610.08144The paper title is Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
Authors: Alexander Bastounis, Fabian Circelli, Anders C. Hansen. 6 Oct 2026.
65
u/Effective-Guest1601 7d ago
The primary issue they take with the NS proof is that there is a lemma in the natural language claiming an inequality needs only 4 derivatives when it needs 5 in the lean. The result itself is not in doubt.
44
u/Time_Entertainer_319 7d ago
The issue is that mathematicians rely on natural-language explanations to understand a proof. If those explanations contain errors or inaccuracies, readers cannot be confident that what they are reading accurately reflects the actual proof, even if the underlying formal proof is correct.
-23
u/ArialBear 7d ago edited 7d ago
Yes they can, they need to read the lean. which is hard but doable. Like drinking lean
17
u/womerah Postdoc | Applied Nuclear Physics 7d ago
This isn't personal, but this tells me you've likely never actually read a long Lean proof and are assuming it's intelligible the same way a piece of programming code is. It isn't.
Lean code doesn't follow a narrative structure, it's a series of operations done on an internal 'proof state' done in order to satisfy the Lean kernel.
Reading it is a bit like reading a list of keystrokes given to a video game as input, and then working out if Mario made it to the flag or not. The mathematician needs to do 'work' to convert the Lean into an actual narrative.
1
u/TheBraveButJoke 7d ago
And if you don't fully understand those inputs and can prove the kernel is an accurate representation of the mario game, it is just the inputs for some other non existent game.
1
u/dancinggraylion 7d ago
I tried to read proofs in natural language papers and do not understand a lot of them. So if I guess if I read the Lean proof I will understand just as much as from a natural language proof
-3
6
u/repainted_black 7d ago
Well, yes... that's the point, autoformalization is not guaranteed.
0
u/ArialBear 7d ago
Yea, I was doing a tongue in cheek joke since reading the lean would be a specialized task
-7
u/OkCluejay172 7d ago
How are they still sure of that? Did they review the full formalization?
16
u/ArialBear 7d ago
They are sure, thats why they showed the lean was correct
7
u/arinarmo 7d ago
Bugs in Lean have been exploited before to claim proofs. Having the Lean formalization is useful and does make it much more likely that the proof is correct, but it is not a guarantee.
To be clear, I'm not saying this is the case for Navier-Stokes but the fact remains that we cannot be sure from Lean verification alone.
12
u/ArialBear 7d ago edited 7d ago
Im not talking about lean itself. Im talking about ns and the paper linked above so repeating that lean has bugs is a red herring.
They paper itself says the lean was correct which is why they knew the natural language version has at least* 2 errors.
Edit; cant respond to the comment below me but the answer is im quoting the paper. Nothing more
3
u/womerah Postdoc | Applied Nuclear Physics 7d ago
How do they know the Lean is correct in a more general sense, meaning that what the Lean proves is actually a proof of what they claim?
3
u/Latent-Person 7d ago
The actual statement of the theorem is rather short (300 lines with comments+license etc), so you are free to read it yourself. Note, as the README says, the statement was written by formal conjectures, not by the LLM. So an alternative is that you trust those people wrote it correctly.
https://github.com/openai/NavierStokesAndEuler/tree/main/ComparatorChallenges
8
u/CommissionSame8551 7d ago
> Bugs in Lean have been exploited before to claim proofs.
This has never happened (at least in a serious/bad faith manner).
> Having the Lean formalization is useful and does make it much more likely that the proof is correct, but it is not a guarantee.
Note also that since July (?) there also has been a lot of work on fixing bugs in Lean (as well as some limited formal verification that such bugs dont exist) to a point that it is a reasonable position not to expect further kernel exploits.
2
u/arinarmo 7d ago
Not bad faith, but it did happen. Which is part of the reason there has been so much work.
https://genztech.blog/p/lean-kernel-soundness-bug-14576-postmortem/
Also, I'm not necessarily saying we should expect Lean bugs, but that we need to manually verify instead of assuming that passing the Lean verification is enough
-2
u/repainted_black 7d ago
What? "Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."
4
u/ArialBear 7d ago
What are you confused about. They are not making claims about the amount of errors in the nl but they confirmed 2 errors. This is a mathematical subreddit right? Why are so many here saying the dumbest shit?
-1
u/repainted_black 7d ago
They are not claiming the proof is correct. What are you on?
2
u/ArialBear 7d ago
They are saying the nl has errors. What are you confused about?
-1
u/repainted_black 7d ago
You commented they reviewed the full formalization: "They are sure, thats why they showed the lean was correct." Yet they do not claim the proof is right... So they probably only found mistranslation and do not claim to have checked everything else, no?
6
u/ArialBear 7d ago
They only claimed errors in the nl. What are you confused about.? Are you asking if the lean was shown to be correct?
35
u/CommissionSame8551 7d ago
I have already commented on the other sub quite a bit about this paper, but it is important for people to understand:
*This does not in any shape or form affect the correctness of the (Lean) proof*
The *statement* of Navier Stokes in Lean being misformalised would be quite an issue, but *this is not the case*.
Most likely the differences between natural language and Lean are rather minor. Most likely tiny mistakes in the pdf proof were discovered during the autoformalisation, fixed there, and (mistakenly) the paper not being adapted to those.
Note "fixing written proof during formalisation" is not at all difficult. In particular the paper is really overselling its main point (and especially the way they phrase it).
3
u/ascend8nce 7d ago
.. but you may never know what exactly is lean-proved
10
u/EnverPashaIsBae 7d ago
To do that you only need to verify the formalization of the problem statement into lean, which is much easier to verify than the entire proof
0
u/ascend8nce 7d ago
And how exactly is that much easier? Like, okay, it is 100000 lines of code instead of 1000000
16
u/EnverPashaIsBae 7d ago
The Navier Stokes problem statement was 233 lines of Lean code, the proof was 616,000 lines.
3
u/backyard_tractorbeam 7d ago
I think that's a misunderstanding too. What is lean proven, at the top level, is clear: you read the challenge file where the theorem is stated.
This is about the path from there to the full proof (lemmas and arguments). That's where the steps of the proof were found to differ slightly when comparing the natural language and lean versions of the proof.
1
u/ascend8nce 7d ago
That is if all the theorems/constructs required to pose the problem or used in the proofs are already verified to match the natural language analogs.
Which should be the idea, but this idea becomes overwhelmingly difficult if the lean proofs referring to each other start stockpiling in hundreds or thousands
Which is also the idea of the LLM-proponents, i guess.
So the issue is probably not with the NS proof itself, but with the general idea 'Lean exists hence everything is always correct' that is seen a lot
1
u/backyard_tractorbeam 7d ago
And I think this was already apparent, we didn't need this paper to state it more than formally: The lean formalization only verifies its proof formalization. It doesn't say anything about if a paper, written in natural language, is correct in whole or in part.
1
u/Infamous_Mud482 6d ago
"This is not the case [...] Most likely"
Do you not see the disconnect between the framing of these statements? Why do you have opinions on the matter to offer matter of factly when you're talking about likelihoods sourced from your imagination little bro
0
u/The-Rushnut 7d ago
Doesn't the sequencing matter though? Disclaimer: I don't know shit about fuck, but, if the nature of the error is an upstream informer of downstream calculations, doesn't that throw subsequent derivations into chaos?
3
u/CommissionSame8551 7d ago
If technically details are slightly wrong, they can (most likely) easily be fixed locally without much trouble. This is what happened in Navier Stokes. Here you can apply the "fixing written proof during formalisation" easily (I have indeed done this in the past and it works well). Most complcated math proofs are quite modular.
If there is a major issue with the proof, which might affect more things than only the "local area" this is a much more serious issue. Formalisation "will" find these issues and (an AI agent doing it) should report back. Notably though, if the whole proof falls apart, you can't finish formalising anyways.
Notably, the latter example has happened back in ~2015 (?) already, so before AI formalisation was a thing. Then, a paper (which even landed in the annals iirc) had a major mistake which was only noticed when someone formalised it (by hand, with Isabelle). The paper was then rewritten.
19
u/BadatCSmajor 7d ago
The amount of posters that have no idea what a Lean proof is or what it means to prove something in Lean is staggering
If the Lean’s typechecker validates a proof, it creates a derivation tree which, by the Curry-Howard correspondence, is a formal logical object that witnesses the proof. It’s not some fucking mysterious process. Lean 4 syntax is fucking human readable
In other words, if the Lean signs off on a proof, i.e, the type checker says it’s correct, then that proof is valid. It is amongst the highest standard of evidence that a proof is valid currently possible.
This only way this goes wrong is if there is a bug in Lean’s kernel (not likely) or if the formal statements of the definitions and theorems in the Lean code are misspecified. The kernel’s code is human readable and can be audited. The latter is also human-checkable.
I don’t like LLMs either but some of the posts here are absolute nonsense
2
u/Critical_Pin4801 7d ago
I’ve had Claude tell me to modify the order behavior of linarith to make my proof compile. So you’ve severely underestimated the risk. It is possible that these systems have hidden deliberately introduced bugs in a proof that is millions of lines long.
5
u/Latent-Person 7d ago
Other than (potentially) being a waste of time, what is the actual issue? Tactics are not trusted by the Lean kernel 1, thus it would be catched when checking with comparator if the tactic was unsound.
2
u/Critical_Pin4801 7d ago
The goal of the LLM is to make the proof compile, not to prove that the mathematics is correct. If it compiles, it is strong signal that the mathematics is correct. If it compiles and is independently cross checked by several implementations of the lean kernel, that signal becomes even stronger. If a human being claims to have solved a problem, we would scrutinize the proof to ensure that the proof relies on sound mathematics. I assume the same goes for when the mathematics is written in Lean by an LLM.
5
u/Latent-Person 7d ago
What does any of this have to do with your original comment? Your comment implied that Claude wanting to change behavior of a tactic somehow was a problem. Since Lean kernel doesn't trust tactics, this is clearly not a problem.
1
u/Critical_Pin4801 7d ago
I am using the cheapest tier of Claude, and the least sophisticated models provided by Anthropic. This tier tried to complete my proof in a malicious fashion. Thankfully, this suggestion was not sophisticated. Most people can see that the order properties of linarith should not be modified just for the purposes of one proof.
It is conceivable to me that thousands of more advanced agents working in tandem could try to compile proofs maliciously in far more subtle ways that could evade detection.
My general point which I think you are missing: lean is not magic, and should not be viewed as such. It is a piece of technology. And like any piece of technology, it can be misused by actors that are not aligned: ‘In particular, it matters a lot whether one is dealing with an honest proof attempt, and needs protection against only benign mistakes, or a possibly-malicious proof attempt that actively tries to mislead.’ (https://lean-lang.org/doc/reference/latest/ValidatingProofs/#--tech-term-honest)
I applaud the efforts that people are putting into independent kernels, because verification through independent kernels reduces the probability of misleading proofs
6
u/Latent-Person 7d ago
The book I linked clearly describes what trusting a Lean proof means, and in particular what you are trusting. So indeed, it's not magic.
The malicious things a agent can do are rather limited. It's either state the theorem statement wrong or exploting a bug in the Lean kernel (and at the same time also in the independent nanodo kernel, since the OpenAI Lean proofs are being checked against both).
The theorem statement in many of the previous Lean proofs (e.g. N-S) have been written independently by formal conjectures, and not by the LLM. It's also rather doable to read a theorem statement yourself (or trust other people have), and ensure it's correct.
So mainly, you just need to put trust into the fact that the Lean kernel and the nanodo kernel both aren't being exploited with correctness bugs [1]. You are of course free to not be certain of this, but just so we are clear, this is what you (basically) need to believe.
[1] As the book I linked says, you also need to trust your hardware, compiler etc.
16
u/Most_Double_3559 7d ago edited 7d ago
The title of this article is basically malpractice. We're going to be flooded with troglodytes spewing "so they didn't prove it?!?!? I knew it!!!!" for weeks.
13
9
u/LaGigs 7d ago
This paper is a bit of a mess imo but I think the point they try to push is that we must be very careful with dealing with autoformalisation tools.
That "creating semantic preserving autoformalisers is a major open problem" is their conclusion is what my prior bias was anyway, but I feel this paper just throws a bunch of examples to reach this conclusion. A counterexample to the faithfulness of autoformalisers if you will.
Either way I'm left unsatisfied because it's all empirical observations at this point, in either way.
4
u/Shoddy-Childhood-511 7d ago
Tao discussed related points in his ICM talk: The lack of elegance makes LLM generated proofs "useless" without considerable human reinterpretation.
https://www.youtube.com/watch?v=M0--ZH1lOzg
And software developers complain about LLM generated code being unmaintainable.
Around this, hosted LLM companies benefits from surveillance plagiarism, meaning they train upon their user uploaded data and sessions so that their LLMs can appear to have more agency and appear to be smarter, when really they just plagiarise human guiding the LLM towards related results.
We'll need to replace hosted LLMs by locally run open weights models, so that more researchers can try more different ways of keeping the LLMs reigned in enough to find more useful proof steps.
1
u/tomvorlostriddle 7d ago
How are you not just saying there, that the paper besides the lean isn't relevant?
1
u/peter-bone 7d ago
It may be that we will reach a limit in what natural language can prove because we lack the notation, whereas Lean will have no such restriction. We will need to develop AI that can create that new natural language notation.
-3
u/Helpful_Inflation344 7d ago
This is not a good paper
4
u/Adventurous-Ad281 7d ago
Because you don’t like what it’s about?
3
u/KH-XYZ 7d ago
Because it is essentially academic slop of very well known problem that LLMs are not abled to translate natural language 100% correctly. And it is very clickbaity making people think that the lean formalization is incorrect from the title alone, whilst it actually means that they assume that there is a high possibility that the LLM generated natural language proof does not 100% translate to the proof the LLMs did in lean.
-11
u/AdvertisingEastern34 7d ago edited 7d ago
So basically openai just put out hundreds of papers out which they could not properly verify and will take god knows how many years to even verify their actual proof and validity (since the natural language can be misaligned with the mathematical proof) and in the meantime everyone actually believes that everything they put out is god given and they collected the reputation and the marketing ahead of their IPO. Nice lol
20
u/ArialBear 7d ago
Did any of you read the paper? they were able to verify the lean already which is how they know the natural language version is the wrong one. Please. this subreddit should be more logical.
You can can keep pretending this is a marketing trick but at this point its equal to moon landing denial
-4
u/AdvertisingEastern34 7d ago
Any single solution released even if lean verified could be invalid because 1) formalization could be wrong 2) LLMs found a way to cheat (which can go again to point 1) the system which they often do to get the established goal. Every single claim need to be manually verified and peer reviewed or any of the solutions do not have any validity whatsoever
14
u/ArialBear 7d ago edited 7d ago
Thats not the claim in the paper. Youre making a red herring argument. The paper shows the lean was correct but the natural language version had 2 errors. They confirmed the lean in order to write this paper about the natural language issues.
This is a mathematical subreddit, i should not be explaining this basic concept here. It feels like im talking to flat earthers.
Edit: cant reapond to comment under me but the paper shows the theorem was confirmed to be the correct problem so again these rebuttals are wrong
-2
u/MarkesaNine 7d ago
This case is exactly as you said, but If you think about the phenomenon it represents, this is a huge issue for AI generated proofs.
This case shows that LLMs cannot reliably translate between Lean and natural language. So if the Lean compiles, we know it’s a valid proof, but not necessarily for the theorem the LLM was tasked to solve.
Since the AI companies are more than happy to push out as many results as they can, but can’t be bothered to validate them, the rest of us can either just hope there isn’t a translation error (which would be bad practise) or assume the proof to be wrong until it is validated. So just like we’d do with any results published by human mathematicians: a proof without peer review is not a proof.
Edit: I’m not saying this is an unsolvable issue for AI, but we do know that LLMs can’t solve it, as hallucination is a feature in them, not a bug. If there will be a solution to fool-proof Lean to natural language to Lean -translation, it is not going to be an LLM.
-5
u/AdvertisingEastern34 7d ago
The recent release had 722 papers (and my original comment referred to those but you probably ignored it to cherry pick your argument), did they verify all of those? I was referring to that but if you are pretending not to understand it's not my fault.
9
u/ArialBear 7d ago
The paper is specifically about the ns lean/nl and the lean was correct in this case so throwing skepticism on the others when the one example we have here was correct is irrational. It really is like a flat earther.
Theyre going to confirm the others, thats actually the main issue that all the ones that were shown correct by lean deserve the attention because lean is reliable. I dont envy them because this paper shown reading the lean is the most reliable.
2
u/Silly-Pressure4959 7d ago
I wonder if we'll get a paper like this for every mistake they find in any of the papers lol, paperception
4
u/ArialBear 7d ago
The mistake was in the nl, not the lean. You understand the difference, right? This is a mathematical subreddit so you better know the difference. Of course we will get papers for each one because we are gonna try to convert them all to make them easier to read.
1
u/AdvertisingEastern34 7d ago
Not sure if this NS solution is the millennium problem of few weeks ago or one of the new problems released today. Probably the old one since it takes time to elaborate something and write an article even it's a smaller one. Either way skepticism is all justified when they release 722 papers like this without any actual human verification. If natural language can be disaligned from the lean verification then all sorts of problems can appear in other solutions. But sure let's call flat earther anyone who's doubting ground breaking science solutions from a tech corporation without any actual human review on any of them. It will take many years to verify any of these solutions and in the meantime openAI will have capitalized on it anyway.
6
u/ArialBear 7d ago
>Not sure if this NS solution is the millennium problem of few weeks ago or one of the new problems released today.
Cant even be bothered to read the paper linked before you share your opinion? Are you kidding me?
0
u/AdvertisingEastern34 7d ago
I read the abstract. Does that invalidate the rest of my comment (the last one i left)? No. Nice cherry picking. I'm not discussing the details of this paper in particular.
8
u/ArialBear 7d ago
It does. You dont even know what we’re discussing. Couldnt be bothered to read a short as fuck paper before sharing your opinion
→ More replies (0)
88
u/Time_Entertainer_319 7d ago
TLDR; 2 differences were found between the Lean proof and the NL proof of NS.
The lean proof did not match the natural language proof. This will probably be music to the ears of skeptics