undefined

points

[-]

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?

by traes1 hours ago|

parent|

[-]

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.

by latent-person4 hours ago|

parent|

prev|

[-]

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

by famouswaffles2 hours ago|

parent|

prev|

[-]

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.

by incognition22 minutes ago|

parent|

prev|

[-]

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.

by runarberg5 hours ago|

parent|

prev|

[-]

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.

by famouswaffles4 hours ago|

parent|

[-]

[flagged]

by runarberg4 hours ago|

parent|

[-]

I don’t. But I do know how the scientific method works, and OpenAI’s display is anything but. Until what they have demonstrated is reproduced I take their claims to be nothing but marketing. A for profit company will lie in order to maximize their profits. Above I presented an alternative hypothesis, which is probably wrong, but until OpenAI’s results are replicated I will believe my alternative hypothesis just as much as I believes the claims of the for profit company making them.

by phoghed3 hours ago|

parent|

[-]

I’m a non-math layman, and not a scientific method knower like yourself. How does one usually “replicate” a math or Lean proof?

by bordercases2 hours ago|

parent|

[-]

Hopefully not in the same way you should never naively trust compilers!

by runarberg2 hours ago|

parent|

prev|

[-]

The generation of the proof can be replicated. And if it can‘t we should be suspicious of their claims.

by nyeah4 hours ago|

prev|

[-]

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

by measurablefunc5 hours ago|

prev|

[-]

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

by aureianimus5 hours ago|

parent|

[-]

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.

by measurablefunc2 hours ago|

parent|

[-]

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.

by auggierose5 hours ago|

parent|

prev|

[-]

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?

by ziiinq5 hours ago|

parent|

[-]

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

by auggierose1 hours ago|

parent|

[-]

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.