| ▲ | buzzy_hacker 8 hours ago |
| If I'm understanding correctly, this is questioning the equivalence between the natural language proof and the lean proof, but not the correctness of the lean proof? |
|
| ▲ | caughtinthought 8 hours ago | parent | next [-] |
| If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim? From the paper:
"A third possibility is that the NL proof provides stronger statements than what the formal proof actually establishes,
with (of course) different proofs. The latter happens in OpenAI’s announced proof of blow-up of Navier Stokes equations." |
| |
| ▲ | hyperpape 8 hours ago | parent | next [-] | | The material is interesting, but unless the statement that is proved in lean is not blowup for Navier-Stokes, then it's still proven. What the examples seem to show is that the proof method is different between the natural language proof and the lean proof. Which, if the lean proof actually proves blowup, would suggest that the natural language proof is subtly wrong, but the strategy was close enough to be used to create a real lean proof. A little worrying, but part of the purpose of formalizing things in Lean, it forces you to be more accurate than natural language does. It's surprisingly common for major theorems to have slight inaccuracies early on that can be repaired. Famously, the initial proof of Fermat's Last Theorem had a flaw that took a year to repair (though I think that's unusually difficult). So the most fundamental question is: does the Lean theorem faithfully state the right theorem? | |
| ▲ | dcre 6 hours ago | parent | prev | next [-] | | Not quite — the formal statement of the problem in Lean may be correct, and therefore the Lean proof gives quite a lot of confidence that the statement is true. It's just that the proof given in natural language doesn't necessarily match up with the Lean proof, so the natural language proof might be unsound even though the statement it's proving is true. | | |
| ▲ | icedrift 5 hours ago | parent [-] | | I was having trouble wrapping my head around it but this cleared it up. |
| |
| ▲ | ammar2 8 hours ago | parent | prev | next [-] | | That assumes the natural language paper came first and then was formalized in lean. I haven't looked too deeply into how these labs solve these problems (or if they even specify this publicly) but you could also start with lean and then write the natural language proof based on it. For what it's worth the initial lean specifications for the top-level theorems generally come from human written formalizations such as in https://github.com/leanprover-community/mathlib4/blob/021ce6... so we can be reasonably confident about their correctness. | |
| ▲ | empath75 8 hours ago | parent | prev [-] | | > If the lean proof doesn't match the natural language one (which is the one the AI generated to solve the problem), it sounds like the lean proof isn't verifying the intended claim? No, the other way around. The natural language proof was derived from the lean code, badly. This is my experience with using claude and lean to prove things. Its natural language explanations drift a lot from the lean, both before and after. But the lean code is the lean code. | | |
| ▲ | latent-person 7 hours ago | parent | next [-] | | > The natural language proof was derived from the lean code, badly. Was it? Are you claiming a LLM does reasoning in lean or what? Since this (and all the other proofs by OpenAI etc) have been in the reverse order [1]: > 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. [1]: https://openai.com/index/navier-stokes-solution/ | | |
| ▲ | caughtinthought 7 hours ago | parent [-] | | Yeah, I was surprised some people think LLMs are reasoning in Lean directly... all their training data is in NL. | | |
| ▲ | ammar2 7 hours ago | parent | next [-] | | It's not that much of a stretch: give the LLM a top-level proposition for the thing you want to prove and have it hack away at it. Each sub-step is verified in lean so you know it's correct. But, the linked post definitely suggests otherwise. That is definitely interesting because how do you know the 88 hours of work are correct before you throw another 17 hours of lean formalization work on it? You could end up just finding out there was some hallucination in the original work. | |
| ▲ | sigmar 7 hours ago | parent | prev | next [-] | | An incredible number of people think that it is reasoning in lean. Argued with several people on this topic. I think they read headlines about lean being used by LLMs and assume it is being used to write the proof. | |
| ▲ | 6 hours ago | parent | prev [-] | | [deleted] |
|
| |
| ▲ | caughtinthought 7 hours ago | parent | prev [-] | | That makes some sense. Given that the vast majority of math in its training data is going to be in NL/latex, I just assumed that the core reasoning happens in NL with occasional LEAN checks to ensure validity. |
|
|
|
| ▲ | OrderlyTiamat 8 hours ago | parent | prev | next [-] |
| The lean proof being correct is easy to verify, whether it proves the thing we care about is much harder. If your code compiles, are you sure it's bug free? |
| |
| ▲ | ndriscoll 7 hours ago | parent | next [-] | | I'm pretty sure Mathlib has had enough human authored definitions to formalize the basic calculus necessary to state Navier-Stokes for quite some time? Some other problems admittedly need quite a bit of machinery built up to even try to say what the question is, but every undergrad learns multiple approaches to formally define everything necessary to write down a PDE. | | |
| ▲ | lanstin 4 hours ago | parent | next [-] | | They do not. Maybe if they take Lean classes? Maybe starting this year they will but my youngest kid is on their like 5th math class in undergrad and hasn't had any lean at all. Not all undergrad math majors even take PDEs; applied maybe, unless you are doing applied discrete math (graphs, combinatorics). | | |
| ▲ | ndriscoll 3 hours ago | parent [-] | | Not Lean specifically, but IMO it's pretty straightforward if you've done math and some programming (and at least my school required some programming). Need to prove a forall statement? forall x, P(x) is the same as a function taking x and returning the proof that P(x) is true. Need to prove an exists statement? Create the pair (x, h) that gives the actual x that proves the exists, along with a proof that it satisfies the property you claim. Maybe the only weird thing is that there are types and sets, so sets are kind of automatically more of a "subset" of some type. The actual Mathlib is more generic, but once you get a hang of writing definitions (as you do in intro proofs), I've found that you can pretty naturally translate whatever you'd have in your undergrad notes. And undergrad should cover defining integers, rationals, reals, relations, functions, sequences, limits, derivatives, integrals, etc. Even if they've never studied solving PDEs, they'd have to take multivariable calculus and know enough to be able to write one (assuming they take at least single variable analysis+linear algebra)? The proofs can get involved and tedious with all of the extra bookkeeping, or techniques to try to reduce the bookkeeping (tactics, etc). But the definitions and statements are pretty much what you'd expect. | | |
| ▲ | IsTom 43 minutes ago | parent [-] | | I'm not sure if calculus of constructions comes naturally to people who didn't have some experience with functional programming. |
|
| |
| ▲ | nyeah 7 hours ago | parent | prev | next [-] | | Not a mathematician, but "pretty sure" might not be good enough to resolve this question. | | | |
| ▲ | 7 hours ago | parent | prev [-] | | [deleted] |
| |
| ▲ | jansport123 7 hours ago | parent | prev [-] | | syntax vs semantics |
|
|
| ▲ | jrflo 7 hours ago | parent | prev | next [-] |
| It doesn't look like they've found an error in the NL proof either, just that they are different? |
|
| ▲ | kccqzy 7 hours ago | parent | prev | next [-] |
| Indeed. The natural language proof is incorrect but the Lean proof is correct. Humans have made similar mistakes too. A human writes a specification for how things should work, the human translates that into code, the code does not work, and finally the human fixes the code and forgets to fix the original spec. |
| |
|
| ▲ | zmgsabst 8 hours ago | parent | prev | next [-] |
| Yes — because there are many non-equivalent statements that are easier to prove. So the Lean proves something and the question is whether that something is actually what we care about — or something similar, but ultimately not the question. |
|
| ▲ | empath75 8 hours ago | parent | prev | next [-] |
| Yes, exactly. There's no real pressure on AI to get the natural language version of the proof correct, and no way to really judge it automatically. |
|
| ▲ | kurtis_reed 7 hours ago | parent | prev [-] |
| Yes however, whether a natural language proof and a formal proof "correspond" is subjective. |
