Hacker News Reader

Comment by ComplexSystems | Hacker News Reader

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.

View on HN

No, they're not claiming that.

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.

If it doesn't correspond to the original proof then you don't know what it is actually formalizing. It could be a buggy proof of ⊥.

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.

This is explicit in the abstract:

> 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]

> the NL proof may be wrong. But who cares?

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 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.

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.

Not necessarily monkeys but thinking in Lean first is quite plausible

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.

it's the result of thinking carefully about the translation process.

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.

If you’ve tried any formalizing in codex Astra often works solely in Lean

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])

[0] https://www.youtube.com/watch?v=kQBu6NH1u3I

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 OpenAI announcement says

> 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)

>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.

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?

This is the formalization that was proven in Lean. As of now at least, it's believed to be a correct statement of the problem.

https://github.com/google-deepmind/formal-conjectures/blob/8...

Nobody is claiming they've misformalized Navier-Stokes.

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.)

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.

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.

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.

> has not formalized the original "natural language" idea of Navier-Stokes incorrectly

Did you mean “not…correctly”?

Nobody has proven or disproven NS equations.

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.

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

Reply on news.ycombinator.com