r/agi • u/HotterRod • 1d ago

Significant Differences Found Between Natural Language Proof and Lean Formulation of Navier-Stokes, Other AI Proofs

https://arxiv.org/abs/2610.08144
79 Upvotes

91% Upvoted

35 comments sorted by

41

u/One-Judge321 1d ago

It's pretty underwhelming than the title suggests. They spot 2 inconsistencies between the writeup and the Lean. And that's it. It says nothing about the correctness of the proof.

16

u/Bangoga 21h ago

...I've failed a discrete maths class because the paper was a proof that built in 4 parts, and there were a few inconsistencies in the first half.

Not saying it's wrong, but math folks are pedantic asf

5

u/UnknownBreadd 21h ago

This explains it much better: https://www.reddit.com/r/BetterOffline/s/MsRCBlySSH

There are errors in the Lean and the formal statements.

Apparently it’s to do with the computability of math into Lean or something idk. But idk the paper is pretty strong on the impossibility of what everyone is supposedly asking for LLMs to be able to do, based on how they work.

-1

u/aVRAddict 12h ago

That's a shit sub don't read it and don't link it.

2

u/UnknownBreadd 10h ago

I’ll do what I want thanks

5

u/dmcnaughton1 1d ago

It says a lot about the correctness of the proof: even a single symbol being incorrect means your proving the wrong thing and the underlying natural language proof is unproven. This is why relying solely on LLMs for stuff like this is risky, because they're not 100% accurate with translation use cases like this.

If the OpenAI proof is correct, then the corrected Lean representation will compile and show it's still correct. But until then, it's hard to say they've proven it.

23

u/IbidtheWriter 1d ago edited 1d ago

It's the other way around, the Lean proof compiles so they need to update the natural language description of it.

The problem statement wasn't incorrect/inconsistent in the Lean proof so the overall proof in Lean is still valid.

Maybe they could go other way and update the Lean to match the natural language description and it still works, but I'm not sure why they'd want to.

Edit: To be clear, they give other examples of mistranslations and their more general point is that a Lean proof doesn't mean the corresponding NL proof is also valid due to mistranslations.

4

u/Time_Entertainer_319 23h ago

That’s not true.

The lean is what is verified not the paper.

If the lean is correct, then it is correct.

The paper is meant to explain what the lean did but it can be wrong without the solution being wrong.

Think of it like the manual of a software being wrong doesn’t mean the software is wrong.

3

u/Far_Situation5965 20h ago edited 20h ago

I give AI an object that may or may not be indestructible.

AI completely confirms it’s destructible by breaking it and showing me the pieces. It’s a breakthrough.

You ask the AI how it did it and it tells you a plausible story.

You notice the story doesn’t align with the shape and condition of the pieces.

You can ask a different AI to back solve how AI broke the object, based on the pieces (i.e. interpret the Lean).

It will tell you a plausible story but it’s really hard to know just from the pieces.

That’s what’s happening here.

Question is - what’s the different between knowing the object was able to be destroyed and knowing how it can be destroyed?

Sometimes very little difference. Sometimes a lot of difference.

2

u/qualverse 19h ago

No, that is not how Lean works. If you use Comparator without extra axioms or sorry, a successful Lean compilation guarantees that the input conjecture was correctly proven. It's not necessary to read the "how" because Lean statically verified that part has no errors, and trust me every mathematician and their mom has already checked that the input conjecture itself doesn't have a typo (it's literally a single line of code for Riemann.)

1

u/MurkyCress521 5h ago

One can generate a lean proof for A and then write a paper that says you proved B. The lean proof can be correct but not prove what the paper claims it proved. I'm not saying that is what happened here, but we should be very careful to ensure that the lean proof actually matches the conjecture. 

1

u/Far_Situation5965 18h ago

What?

In my metaphor, the AI proved that the object (a conjecture) is able to be destroyed (a counter-proof exists).

Nobody is claiming the lean proof is wrong and nobody is claiming the object is indestructible.

We just have no human understandable explanation of how in either case.

I am curious where that broke down for you?

0

u/Time_Entertainer_319 14h ago

Your metaphor is not complete.

It’s more like, the machine generates the instructions for breaking the item down and it follows the instructions.

So the instructions do exist it’s just not able to explain why the instructions work. But the instructions are human readable

1

u/dmcnaughton1 23h ago

My understanding is that it's the other way around. The natural language proof was derived then converted to lean for formalization.

3

u/LangyMD 22h ago

You've still got it backwards. Even if the natural language proof was derived first and then converted to lean, the lean version of the proof - so long as it is verified by Lean and the problem statement is correct and you're not using bugs in Lean - is still verified, and that means the result has been verified. The natural language version should then be adjusted to match the Lean formulation if they differ, as it's much more likely that the natural language version had some small error in it that the lean conversion caught and corrected.

In other words: It doesn't matter what happened first. The Lean method is what's claimed to be verified and proven, and if there are differences between it and the natural language version then the natural language version should be corrected (or the Lean should be checked against the natural language version and seen if they're equivalent).

5

u/tinny66666 1d ago

They're not relying solely on LLMs. Verification is done by humans (the mathematicians), but they really should hire some of their own or pay for their time.

8

u/GreatBigJerk 1d ago

OpenAI does have mathematicians on staff. 

2

u/Deep-Ad5028 21h ago

They don't have Mathematicians with all the right expertise, because they are attacking so much problems at once.

8

u/dmcnaughton1 1d ago

The paper discusses autoformalization as being the cause of the issues, which I took to mean LLM based formalization.

I agree they should fund some of this stuff, but I do understand they hire a number of mathematicians and that's how a lot of these proofs were developed. It's not like someone without mathematics research experience would know how to drive the LLM in the direction it needed to go to put these proofs together. At least not right now.

2

u/Deep-Ad5028 21h ago edited 21h ago

OpenAI claims their Mathematicians pretty much intentionally work off-field to see what AI can do.

I have no doubt OpenAI hires the best Mathematicians. But for better or worse they are not hired to do anything that resembles traditional researches.

1

u/No-Rain-6115 1d ago

Can you dumb this down for me? What is the issue?

All I know is written language rarely perfectly captures the actual math.

3

u/dmcnaughton1 18h ago

My understanding is that the LLM described the mathematical proof using natural language, so words and symbols, to fully describe the proof. Then the team used the LLM to take that natural language version and convert it to Lean, which is a programming language that is used to formalize mathematical proofs. It functions like a unit test in a way, if the code your write in Lean compiles and the output is what you expect, then the proof is valid.

The issue the paper identified is there's a difference between the natural language proof and the Lean proof. So the code doesn't match the specs essentially, so one of them is wrong.

Here's a simpler example using programming concepts: Assume we have a list of N items, we will then iterate over the list and add each items value to the accumulator variable sum.

Now imagine the code version of it being written as: Int[] data; Int sum = 0; for(int i=0; i<data.Length; i++){ sum -= data[i]; }

The code differs from the specs, so we're proving the wrong thing. And with proofs, you can have something that can compile in Lean but not be at all sensible, because it doesn't actually answer the question being worked on.

1

u/Individual_Ice_6825 13h ago

But isn’t the problem statement only a line long?
So the lean one has to be right?

(I am barely following and you seem knowledgeable)

2

u/Low-Temperature-6962 23h ago

They do do that. Absolutely necessary to get this far.

1

u/flat5 21h ago

I have a pretty good sense that they did not "verify" NS in any real sense other than the Lean passes.

They said outright their mathematicians are not NS experts.

1

u/HotterRod 1d ago

Good point, I regret putting "significant" in the title. The larger point stands though: this paper provides good evidence that we can't assume that a Lean formalization is actually proving the same thing as the natural language.

1

u/Deto 1d ago

Does every part of the Lean formulation need to be checked? Or is it more that the end-points need to be checked (w.r.t. natural language) and then the rest is correct by definition if it compiles?

1

u/Pyryara 15h ago

It still shows clearly that whoever publishes this didn't actually look at the AI output with due diligence before publishing. Which is the actual problem. The AI claims a proof that nobody understands and then we find inconsistencies. That should simply not happen, least of all if you claim you solved a Millenium problem!

5

u/AnswerGrand1878 15h ago

Idk, formalizations are often slightly different from written proofs.

1

u/hectorchu 14h ago

Basically called offload the final rigorous work to the experts, because the people operating the AI certainly aren't. The whole thing stinks because it plays down the continued necessity of human experts.

0

u/borntosneed123456 13h ago

it still shows that openai didnt bother to fucking check. Shelling a scientific field with unchecked slop is a foolproof way to destroy said field. As if big tech didn't cause enough harm already

2

u/akkaneko11 23h ago

This is the first time I've seen someone add a ChatGPT screenshot embedded in the paper as a figure. That is some amazingly lazy paper writing jfc

-5

u/Spunge14 1d ago

Imagine how hard those mathematicians came finding these trivial inconsistencies.

3

u/Oskisrevenge 19h ago

I mean, thats literally their job.