Aside from the usual squabbling about AI, it seems the bombshell claim is this:
"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."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
I'm dutch and not understanding his NL thesis, though i think these days its just as easy to let an ai provide a claim that is actually false, it be easier to hack lean then solve some of those solution for an AI
If I understand the abstract correctly (big caveat), they aren't saying they didn't prove it. They're saying they gave two proofs, one in natural language and one in Lean, that are not equivalent to each other. I assume the main significance is that the Lean proof is not a formal verification of the natural language one and the natural language proof is not a readable explanation of the Lean one. Both of those things can be desirable, so to complete the set we'd get 4 proofs.
From computer science perspective the conclusion is obvious: untenable to have two representations without an exact translation or machine checked correspondence between then. All we have is a vibe translation using the LLM. The methodology should obviously be improved.
and clearly the computer science perspective is: get rid of the humans and express everything directly in lean so the computers can keep getting work done!
But just to clarify: is either of them actually addressing the real Navier-Stokes, or will it turn out we'll end up with two pairs of proofs about something irrelevant to the actual problem?
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
It seems the Lean version may not be a correct statement of the Navier-Stokes problem.
They go on to say this--
Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations.
They are claiming that the NL proof and the Lean proof are not consistent though: the NL proof is not being validated by the Lean proof, and the Lean proof is not being "explained" by the NL proof.
Yes it could be that neither the NL proof nor the Lean proof correspond to the actual Navier Stokes problem. Here's a quote from the paper--
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
If I understand well, they mean that the thing they proved in lean is not Navier Stokes. And they don't make any statement about whether the natural language proof is correct or not.
I read them as making a much weaker claim than this: not that the Lean proof isn't valid, just that it is not actually a formalization of the natural-language proof in the PDF they provided alongside it. I haven't heard any PDE people claim that the Lean proof is invalid, and I have heard things from a lot of them that imply that they think it is valid. (I'm a former research mathematician, but this is very far from my specialty, so I'm not really equipped to evaluate this claim myself.)
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
The thing is that Navier-Stokes has a definition split off separate from the formalization, and that is what has been completed. People have looked at the definition of the final statement. This paper only mentions the proof and intermediate statement, not the final statement. The most likely case to me is that intermediate statements do not match, but the end result still holds.
Seems kinda odd then that it didn't occur to OpenAI to iterate until they reached a fixedpoint for both the informal & formal development b/c it's obvious that correspondence should have been part of their training pipeline.
Jesus Christ, so many people here who have no clue what they are talking about.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
> Jesus Christ, so many people here who have no clue what they are talking about.
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
No. What the paper says is that in principle, translating NL statements to Lean statements is hard. Nobody doubts that, translating informal to formal text cannot be formally proven correct, so...
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
> 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.
Could /I/ be mistranslating the paper’s formal statement to NL? I don’t think so, but in case I am wrong, feel free to cite the correct formal statement that they claim as divergent between Lean and NL formulations by OAI.
Yes, you are misunderstanding what the paper claims. Navier Stokes for example is not such an example, only the proof is different. For their other examples, none of them they claim that they concern actually the open ai solved theorems. You are welcome.
And yet I cited a specific statement made concerning N-S specifically, whereas all you’ve done is make patronizing remarks, and strawman arguments.
Have you actually read it? They give a handful of examples of mistranslations of both claims and proofs thereof, in relation to NS and Euler, though I do concede that they do not go as far as claiming outright the NS statement itself is mistranslated.
Unfortunately, lean proof alone is not enough. sidestepping the raging discussion regarding the meaning of mathematics, just because the lean compiles is not proof in itself that it is correct in the sense that mathematicians mean. Unless of course, you can prove that lean itself is correct, which you can’t.
we have seen “proofs” earlier this year that essentially abused some bugs in the kernel. it would be very convenient if every program written in rust was automatically correct if compiles - something i strongly suspect you believe - unfortunately, this is not the case for either.
In case you are not aware, the actual theorem statement of N-S was never translated by an LLM, but was written independently by formal conjectures, as they say in the README [1].
A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).
We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).
It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.
edit:
Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.
2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).
In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.
As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).
So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.
[1] As the book says, you also need to trust the hardware, firmware etc.
You may be overconfident here. The NL paper may be properly stating the Navier Stokes problem, and the Lean code may not be.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
Why would they do that, knowing that the one known to be correct is the Lean one? Just to claim that the (correct) Lean proof did not translate well to English? That would be weak, and a colossal waste of energy and time.
Why do people program in Python instead of writing machine code?
Why are review papers published? Executive summaries? "Introduction to X" books?
People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.
It reminds me of how provably secure software was all the rage for awhile. Until people found that the idealized system/lemmas were so far from reality that the proved security was worse than meaningless because it gave a false sense of security.
In order to prove security, you must first simulate the universe.
Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.
The statement written in Lean, is not actually a correct description of the Navier-Stokes problem. It's some other easier statement. That's why the Lean code may not be a proof.
Here's a quote from the paper.
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
"Tracing the proof of (3.3) we find that the series arises from applying the Lean theorem coefficient_seminorm_bound, just as Figure 3 mentions. Consequently, the Lean results discussed in this section are weaker than (3.1) in the NL proof."
So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?
Here is their remark.
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
The "statements" here are statements of lemmas, not the statement of the main theorem. The main theorem statement was written by humans (prior to the OpenAI work), so there shouldn't be any concern that an AI mistranslated it.
So, the AI wrote a NL proof of Navier-Stokes, then incorrectly auto-formalised it to Lean, but still ended up with a verifiable proof of Navier-Stokes? That seems... strange?
Or maybe the AI didn’t write Lean proof at all, or rather, not the LLM at least. But instead OpenAI has an internal traditional reinforcement model that is able to stumble on the Lean proof by the share amount of compute power available to them thousand monkeys on a thousand typewriter style. And then pretend LLM did it because that is what they are selling.
Or the AI wrote a NL proof of Navier-Stokes, began rewrite in Lean, then discovered a false / handwavy / easier to write in Lean / etc approach of some parts of the proof, and modified it accordingly. Since there wasn't any backpass from Lean to NL to include any changes it did due to any of the above reasons, the proofs aren't identical. That's what I think is most likely.
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
It's not actually the same model that solved the problem that did the translation. Astra did the translation after the intenral model produced the NL Proof. As for the discrepancies, It's not necessarily right to think of this as 'incorrect formalisation'. Maybe it was essentially a 'proof refactoring'. Maybe Astra thought some parts could be easier expressed in a certain way, or maybe aspects of the NL proof were kind of handwavey etc.
This same thing happened back in the 10 advances in math and CS release a month or two ago. The non sofic group construction relied on false prior literature. They realized this and fixed it in the lean program but didn't modify it in the writeup, so the written proof was both incorrect as stated and did not correspond to the lean proof. I was surprised how little press it got at the time, it seems like a huge risk factor.
I don't know if we can really be clear about the order of things, but I think even without AI maths is filled with "someone provides a proof of X, and the proof itself is wrong/incomplete but X itself is true".
"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.
The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.
EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])
I would expect it's the other way around. The AI wrote a Proof of NS in lean and write up a NL proof based on the lean one. The authors claim that openAI did NL -> Lean, but that is unsubstantiated.
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
This seems pretty clear that they found the proof first and then mechanized it afterwards.
Trying to map this observation to code and appreciate them starting with very simple examples (that Astra screw-fixed into lean.)
But in a simplified way this is close to promting the model to create a set with the members 1,2,1,5 and it correctly creates {1,2,5} in code. So The initial "proof" / instruction was wrong and it silently fixed that. ( Which is one of the failure modes they're describing)
e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.
Why do you assume this order? I would assume the AI starts with lean (that's what it was RL'd on at least) then tried to translate the proof for us humans, which is quite hard.
I'm not sure about it but it seems plausible given the potential error.
Edit: they explicite say that your order is correct in the post
Proof steps can become different in Lean but still work to prove the theorem. Incorrect proof steps in the NL paper could also be converted to correct ones in Lean. The paper shows some examples of this. So the NL paper can't be trusted even if Lean verification passes, but it doesn't immediately mean that the NL proof is wrong or that Lean is checking the wrong thing.
>No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
This doesn't answer the question. The question was: what was the difference in A and B. Your answer looks like this:
A: The English language description doesn't do the same thing as the code the AI wrote.
B: The English language description doesn't do the same thing as the code the AI wrote.
A and B are the same; there is no difference. Is this what you meant? Or did you mean the opposite of this? If you meant the opposite of this, what exactly is the difference?
They published both a natural language proof and a lean proof. This paper says the NL proof does not match does not match the lean proof, using different arguments and some stronger claims. It does not claim the lean formulation of NS or the rest of the lean proof is invalid.
"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."
You didn't answer the question. Quoting from upthread:
A: "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."
B: "No, they're not claiming that [...] The authors are claiming that the Lean proof is not the same proof as the NL one"
The question was: what's the difference between A and B?
Your answer to that question was "This paper says the NL proof does not match does not match the lean proof".
It seems to me like A is the exact same thing as B, and you are here claiming that they're different things while merely repeating the same claim that was already claimed in both A and B.
3) The comments promise functionality the code does not implement.
The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"
> No one is disputing that the Lean formalization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?
Well the theorum statement (what it proves) is short and easy to verify. I would not be surprised if hundreds of mathematicians have looked at it at this point.
Which is exactly why you want a Lean proof in the first place!
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.
My understanding is that the statements in the Lean proof might not actually correspond to the Navier-Stokes problem. And that requires mathematical insight to be able to verify, which could take quite a while.
The claim is about the equivalence between two proofs and says nothing about the correctness of either proof. This seems to be confusing a lot of people.
NS is continuous approximation to what is otherwise a discrete system. Particle collisions are discrete time events that are averaged over time. NS loses accuracy for very, very, very very low fluid densities and energies.
AI "proving" that this approximation can numerically "blow" up does not mean the approximation loses validity.
Navier-Stokes is an equation, not a theorem, so there is no such thing as "a proof of Navier-Stokes". The equation is a partial-differential-equation model of viscous fluid flow. Its correctness has never been in doubt: we know it cannot possibly be an exact description of real fluid flow, that it's a pretty good approximate description, and that there exist well-behaved solutions for a number of initial conditions.
What OpenAI purports to have proven, as I understand it, is that certain initial conditions to that equation, plus "forcing" over time (which could be a literal force acting on the fluid such as stirring it with a spoon or some other extrinsic effect) only have finite (and therefore physically plausible) solutions for a finite period of time, after which singularities appear, with the velocity or pressure of some of the fluid approaching infinity as you approach the finite time limit.
I think we can be pretty confident that the L∃∀N proof is really about Navier-Stokes. The question is whether what it says about Navier-Stokes is what we think it says.
Agreed. It'd be super cool to see a Firefox/Chrome extension look for Latex equations on sites you were browsing and then cross-reference them against wiki/etc. and give them the math-equivalent of syntax highlighting.
Even more so if it worked with PDFs.
I already have way too many projects on the backburner right now... wink wink nudge nudge to anyone who wants to take this.
If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof?
If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
From the paper:
"A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes,
with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
The material is interesting, but unless the statement that is proved in lean is not blowup for Navier-Stokes, then it's still proven.
What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof.
A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult).
So the most fundamental question is: does the Lean theorem faithfully state the right theorem?
That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it.
For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.
> If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim?
No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.
That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity.
> The natural language proof was derived from the lean code, badly.
Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
It's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise.
That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
An incredible number of people think that it is reasoning in lean. Argued with several people on this topic. I think they read headlines about lean being used by LLMs and assume it is being used to write the proof.
If you have ever worked with claude code and lean, it goes back and forth between lean and NL reasoning. I have done a few proofs with claude and it almost _never_ gets the argument right in prose. It usually has to go into lean and grind through proof obligations and then it finds problems, work arounds etc.
Not quite — the formal statement of the problem in Lean may be correct, and therefore the Lean proof gives quite a lot of confidence that the statement is true. It's just that the proof given in natural language doesn't necessarily match up with the Lean proof, so the natural language proof might be unsound even though the statement it's proving is true.
I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE.
They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics).
Not Lean specifically, but IMO it's pretty straightforward if you've done math and some programming (and at least my school required some programming).
Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true.
Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim.
Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type.
The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)?
The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect.
Yes — because there are many non-equivalent statements that are easier to prove.
So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.
Indeed. The natural language proof is incorrect but the Lean proof is correct.
Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.
The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
> That's not a trivial if: stating the problem precisely is often as hard as the proof.
Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.
This paper is a large amount of nothing. First, natural language is not as precise as lean, so you have multiple ways to translate a NL argument to Lean. As shown in Fig 1, the LLM did a decent job at translating the argument about roots in a succint way.
Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean ones. My understanding is that the translator LLM got lazy and wrote the minimal amount of code that satisfied the theorem without the extra stronger claims.
It is common in mathematical papers to say "And by the way, this actually proves [stronger claim]", but this is something an AI with a precise goal of performing a translation would never do, as it's goal is to translate the proof, not to quality mathematics.
- The lean kernel could always have a bug.
- The formalized statement may not correspond to what _mathematicians_ "actually
wanted"
It seems natural to make the argument of, "Well, even if you make the argument
that the proof can have mistakes, it's surely easier to check the problem
statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments
correct" according to the _second_ criteria - maybe in the natural proof it
invents an object subtly different from the formal one, but it all checks out.
If you guarantee that the _original_ statement corresponds, then the only
possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have
good theories for? How do you quantify how much descriptive power you need to
express a question? Often times in math, the hard part is getting the definition
right - but what if the definition itself starts to become so complex and
unverifiable that no one can correspond that to anything? Well, it seems like
many interesting long-standing math problems have "relatively" simple problem
statements, in such a way that you could formalize it to lean easily, but not
sure if there's really a silver bullet w/ lean or if it's going to be turtles
all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more
general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its
a generalized theory of semantics.)
Given the high-level description of the examples, I think it's less of a "mis-translation" as it is the LLM tweaking the proof as it formalized it. Going between m+4 and m+5 is a pretty different thing than the sort of ambiguities that generally arise in parsing natural-language mathematical statements.
215 comments
"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."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.
Did you mean “not…correctly”?
;)
https://github.com/google-deepmind/formal-conjectures/blob/8...
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
It seems the Lean version may not be a correct statement of the Navier-Stokes problem.
They go on to say this--
Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations.
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
No one is disputing that the Lean formaization of Navier-Stokes is correct, so we should have high confidence that the generated Lean proof is valid.
The authors are claiming that the Lean proof is not the same proof as the NL one. Therefore, we shouldn't yet have confidence that the NL proof is valid.
This is an important claim which the math community will need to work through. However, the Lean proof alone is sufficient for OpenAI to (reasonably confidently, leaving aside questions of academic manners) claim to have proven NS.
A proof of a theorem is different from the statement of the theorem. OpenAI has a Lean proof of the statement. That is all they need. There may be many different proofs of this statement, including NL proofs. It does not matter that these NL proofs may or may not be different from the Lean proof, at least for the correctness of the Lean proof. But of course the NL proof may be wrong. But who cares?
Indeed. If only some of those people would see the irony.
What matters most of all, as any first year student of mathematics would know, is whether the formal problem statement corresponds to the NL statement. TFA specifically states that at least some of the allegedly proven formal statements DO NOT.
Does the paper give a single example of one of the OpenAI solved theorems with a Lean certificate where the Lean statement does not correspond to the actual statement from the mathematical literature? I don't think so, but in case I am wrong, feel free to provide that example.
> 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.
Could /I/ be mistranslating the paper’s formal statement to NL? I don’t think so, but in case I am wrong, feel free to cite the correct formal statement that they claim as divergent between Lean and NL formulations by OAI.
[edit: typo]
And yet I cited a specific statement made concerning N-S specifically, whereas all you’ve done is make patronizing remarks, and strawman arguments.
Have you actually read it? They give a handful of examples of mistranslations of both claims and proofs thereof, in relation to NS and Euler, though I do concede that they do not go as far as claiming outright the NS statement itself is mistranslated.
Unfortunately, lean proof alone is not enough. sidestepping the raging discussion regarding the meaning of mathematics, just because the lean compiles is not proof in itself that it is correct in the sense that mathematicians mean. Unless of course, you can prove that lean itself is correct, which you can’t.
we have seen “proofs” earlier this year that essentially abused some bugs in the kernel. it would be very convenient if every program written in rust was automatically correct if compiles - something i strongly suspect you believe - unfortunately, this is not the case for either.
A Lean proof has a much higher probability of being correct (in my opinion) than any published (either preprint or peer-reviewed) paper, yet no one before LLMs were walking around claiming every result published can't be trusted yet (without an actual reason).
We have seen one such instance of Lean bugs, which was found adversely against Lean (as in find bug then use this bug to prove Collatz, not just found when being asked to prove it).
It's also worth to note that the way N-S (and all the other proofs by OpenAI etc) have been found is first prove it in NL then translate to Lean. I.e. it would have to first believe it found a correct proof in NL, and then afterwards either accidentally or on purpose use a Lean kernel bug.
[1]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
edit: Probably also worth to mention that the proof have been checked both by the Lean kernel and the independent nanoda kernel, so it would need to exploit bug(s) from both.
Define “correct” in this context. That’s the real problem here.
Here is what putting trust into a Lean proof means https://ammkrn.github.io/type_checking_in_lean4/trust/trust....
In particular the main ones are:
1. The theorem has been written correctly.
2. No exploit of a kernel soundness bug in Lean (and the independent kernel nanodo, which OpenAI also checks against).
In particular, if you trust this, then you don't need to care about anything else the Lean program does, no matter how many lines, lemmas etc. it makes along the way.
As I said above, the theorem statement have been written independently by formal conjectures, and you are free to read it yourself (or trust other people have done it).
So, assuming you don't disagree the theorem statement have been written correctly, you pretty much need to believe 2 is false, if you don't trust the proof [1]. And that's what I find has a rather low probability personally.
[1] As the book says, you also need to trust the hardware, firmware etc.
Here's from the paper--
3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement.
The people trying to understand the proof are probably following the natural language version. So they care.
I wouldn’t be surprised at all if that’s how this paper (which I did not read) arose.
Why are review papers published? Executive summaries? "Introduction to X" books?
People's time and computational resources are finite. Summarising information -- ideally in structured ways that preserve important properties, but even in informal, unstructured ways -- is critical for making any kind of progress in this world.
In order to prove security, you must first simulate the universe.
Everyone. I don't think many people working in fluid dynamics were surprised you can find a blow-up in Navier-Stokes. What would advance human knowledge is understanding the situations in which a blow-up might occur. In that context, the lean proof is necessary, but the non-lean proof is more important.
Here's a quote from the paper.
"3.1. When the NL paper declares stronger statements than what Lean proves
We commence with an example that complements those in §2. In the following example the AI autoformalisation results in a different Lean proof of a weaker statement."
"Tracing the proof of (3.3) we find that the series arises from applying the Lean theorem coefficient_seminorm_bound, just as Figure 3 mentions. Consequently, the Lean results discussed in this section are weaker than (3.1) in the NL proof."
So the question is, was the Navier-Stokes problem framed properly in the lean code, or is some easier problem represented in the Lean code?
Here is their remark.
"Remark 3.4 (Further potential mistranslations of the Navier-Stokes proof). The above examples require careful manual checking of both the NL proof as well as the Lean proof, which is delicate and highly time consuming. Moreover, the fact that we display only two examples does not mean that these are the only cases of mistranslations."
If the reason for the differences was done intentionally in Lean (as opposed to hallucinate e.g. m+4 vs m+5 as mentioned in remark 3.2), then a simple recording of differences, and then afterwards pass back any changes to the original NL would fix the issue. If it was hallucinated, then there is no guarantee it wouldn't keep hallucinating, and thus you might never end up with the same proof no matter how many passes you do back and forth (see remark 3.4).
humans as a whole have always known the weakness of natural language is in its precision. In a way this isn't strange that this issue has come up.
"Incomplete" proofs might be a way of viewing this. You have a NL argument to prove X. It turns out the NL proof has holes you can drive a truck through. So... you go around and patch the holes.
The resulting proof is different! You can start off with a bad proof and find a correct proof. Sometimes.
EDIT: for French speakers (maybe autodub gets you there) I saw a very nice simple case of this recently. A commonly stated proof for a relatively simple theory. The proof has a giant hole in it, and completing it requires some work [0])
[0] https://www.youtube.com/watch?v=kQBu6NH1u3I
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
This seems pretty clear that they found the proof first and then mechanized it afterwards.
e.g. one of the lemmas in the NL description is false, but a weaker version of the lemma (that does hold) is sufficient for the proof, so the (incorrect) lemma is never formalized.
I'm not sure about it but it seems plausible given the potential error.
Edit: they explicite say that your order is correct in the post
These authors don't seem to be disputing that this Lean formalization of Navier-Stokes is correct. I don't think that gives us any new information about whether the generated Lean proof is or isn't a valid proof of this N-S blowup thing.
A: The English language description doesn't do the same thing as the code the AI wrote.
B: The English language description doesn't do the same thing as the code the AI wrote.
A and B are the same; there is no difference. Is this what you meant? Or did you mean the opposite of this? If you meant the opposite of this, what exactly is the difference?
"The Lean code merely tells us that the theorem is correct, yet the NL proof with intermediate arguments, lemmas and results may be incorrect or have incorrect arguments."
A: "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."
B: "No, they're not claiming that [...] The authors are claiming that the Lean proof is not the same proof as the NL one"
The question was: what's the difference between A and B?
Your answer to that question was "This paper says the NL proof does not match does not match the lean proof".
It seems to me like A is the exact same thing as B, and you are here claiming that they're different things while merely repeating the same claim that was already claimed in both A and B.
1) The code and the comments disagree.
2) The code passes the tests.
3) The comments promise functionality the code does not implement.
The first post was "It doesn't meet the business requirements the comments indicated, so the software is broken." The replying post was "Actually, the business requirements were faithfully turned into tests, so the software is fine. The comments need to be rewritten"
Why? It is a correct proof. Is it a correct (dis-)proof of NS? These statements do not seem particularly related. People, including (especially?) mathematicians, find NL proofs far easier to read than Lean proofs. I would bet the ratio of people who read (part of) the NL proof vs the Lean proof is at least 100 to 1. It seems incredibly unlikely that anyone has read and reviewed the whole Lean proof (including the authors of the OP).
Is it particularly easy to see that the Lean proof does actually disprove NS, rather than proving something similar but not the same?
NL proofs rely on not-entirely-correct prior art, and contain countless holes both big and small. When formalizing human NL proofs it is probably very normal that the Lean proofs doesn't quite follow the NL proof.
NS is continuous approximation to what is otherwise a discrete system. Particle collisions are discrete time events that are averaged over time. NS loses accuracy for very, very, very very low fluid densities and energies.
AI "proving" that this approximation can numerically "blow" up does not mean the approximation loses validity.
What OpenAI purports to have proven, as I understand it, is that certain initial conditions to that equation, plus "forcing" over time (which could be a literal force acting on the fluid such as stirring it with a spoon or some other extrinsic effect) only have finite (and therefore physically plausible) solutions for a finite period of time, after which singularities appear, with the velocity or pressure of some of the fluid approaching infinity as you approach the finite time limit.
This is a result that Terry Tao conjectured in 02014, but without the forcing: http://arxiv.org/abs/1402.0290
I think we can be pretty confident that the L∃∀N proof is really about Navier-Stokes. The question is whether what it says about Navier-Stokes is what we think it says.
More interesting, you can ask a vision model to color parts of speech in img2img and it works OK for frontier models.
Even more so if it worked with PDFs.
I already have way too many projects on the backburner right now... wink wink nudge nudge to anyone who wants to take this.
I don’t think that actually explains the idea of a momentum density transport equation well at all.
From the paper: "A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes, with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations."
What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof.
A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult).
So the most fundamental question is: does the Lean theorem faithfully state the right theorem?
For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness.
No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code.
Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]:
> The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT‑6 Astra.
[1]: https://openai.com/index/navier-stokes-solution/
That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work.
If your code compiles, are you sure it's bug free?
Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true.
Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim.
Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type.
The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)?
The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect.
So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question.
Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
Really? You think 300 lines of Lean code [1] is just as hard as the proof (or even remotely close)? Also note, as the README says [2], that the theorem was written independently by formal conjectures, not by the LLM.
[1]:https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
[2]: https://github.com/openai/NavierStokesAndEuler/blob/main/Com...
Moreover, the paper claims that the NL arguments of Navier-Stokes are stronger than the Lean ones. My understanding is that the translator LLM got lazy and wrote the minimal amount of code that satisfied the theorem without the extra stronger claims.
It is common in mathematical papers to say "And by the way, this actually proves [stronger claim]", but this is something an AI with a precise goal of performing a translation would never do, as it's goal is to translate the proof, not to quality mathematics.
_Assuming_ two failure modes:
- The lean kernel could always have a bug. - The formalized statement may not correspond to what _mathematicians_ "actually wanted"
It seems natural to make the argument of, "Well, even if you make the argument that the proof can have mistakes, it's surely easier to check the problem statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments correct" according to the _second_ criteria - maybe in the natural proof it invents an object subtly different from the formal one, but it all checks out. If you guarantee that the _original_ statement corresponds, then the only possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have good theories for? How do you quantify how much descriptive power you need to express a question? Often times in math, the hard part is getting the definition right - but what if the definition itself starts to become so complex and unverifiable that no one can correspond that to anything? Well, it seems like many interesting long-standing math problems have "relatively" simple problem statements, in such a way that you could formalize it to lean easily, but not sure if there's really a silver bullet w/ lean or if it's going to be turtles all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its a generalized theory of semantics.)
"Disclaimer: We do not make claims about the correctness of OpenAI’s NL proof, we only make statements about mistranslations into Lean."