upvote

points

by measurablefunc5 hours ago |
comments
upvoteby aureianimus4 hours ago|
next
[-]
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.
reply
upvoteby measurablefunc1 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.
reply
upvoteby auggierose4 hours ago|
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?

reply
upvoteby ziiinq4 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.

reply
upvoteby auggierose54 minutes 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.

reply