| ▲ | measurablefunc 11 hours ago |
| 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 ⊥. |
|
| ▲ | aureianimus 10 hours ago | parent | 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. |
| |
| ▲ | measurablefunc 7 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. |
|
|
| ▲ | auggierose 10 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? |
| |
| ▲ | fn-mote 4 hours ago | parent | next [-] | | > 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. | | |
| ▲ | utopcell 2 hours ago | parent [-] | | 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. | | |
| ▲ | akoboldfrying an hour ago | parent [-] | | 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. |
|
| |
| ▲ | aeternum 2 hours ago | parent | prev | next [-] | | 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. | |
| ▲ | ziiinq 10 hours ago | parent | prev [-] | | > 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. | | |
| ▲ | auggierose 6 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. | | |
| ▲ | ziiinq 2 hours ago | parent [-] | | 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] |
|
|
|
