Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- Hm, looking through here, I don't see where they state what it is that OpenAI actually proved instead of Navier-Stokes blowup with forcing. I see where they do this for some other particular statements used along the way, but not for the headline result.by Sniffnoy
- Given the high-level description of the examples, I think it's less of a "mis-translation" as it is the LLM tweaking the proof as it formalized it. Going between m+4 and m+5 is a pretty different thing than the sort of ambiguities that generally arise in parsing natural-language mathematical statements.by dooglius
- Will we ever run into a theory of meaning crisis?
_Assuming_ two failure modes:
- The lean kernel could always have a bug. - The formalized statement may not correspond to what _mathematicians_ "actually wanted"
It seems natural to make the argument of, "Well, even if you make the argument that the proof can have mistakes, it's surely easier to check the problem statement of something rather than the solution".
(A "nice property" is that, the agent doesn't need to even get "subarguments correct" according to the _second_ criteria - maybe in the natural proof it invents an object subtly different from the formal one, but it all checks out. If you guarantee that the _original_ statement corresponds, then the only possibility is the lean kernel. So it doesn't recurse infinitely, in this case).
But "definitions" are always a really weird thing that I don't think we have good theories for? How do you quantify how much descriptive power you need to express a question? Often times in math, the hard part is getting the definition right - but what if the definition itself starts to become so complex and unverifiable that no one can correspond that to anything? Well, it seems like many interesting long-standing math problems have "relatively" simple problem statements, in such a way that you could formalize it to lean easily, but not sure if there's really a silver bullet w/ lean or if it's going to be turtles all the way down.
It probably doesn't matter as long as AI keeps skyrocketing on the much more general property that is "intelligence", but still. Interesting to think about.
(Well, this is where AIT gets actually interesting, but still, I don't think its a generalized theory of semantics.)
by sigbottle - The paper shows that the Lean proof and the prose (pdf) proof do not match exactly. But if the Lean theorem Lean accepted is equivalent to original problem statement published by the Clay Institute, this mismatch is of no consequence to the validity of the proof itself. That's not a trivial if: stating the problem precisely is often as hard as the proof. Validation efforts should concentrate on whether the Lean theorem is equivalent to the one published by the Clay Institute.
That said, a gap between the Lean proof and the pdf is annoying for interpretability, and interpretation is a valid aim, but that does not factor into the proof's validity.
by infogulch - For a refreshment of what is Navier-Stokes in a few words: https://p.migdal.pl/equations-explained-colorfully/#navier-s...by stared
- 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?by buzzy_hacker
- Aside from the usual squabbling about AI, it seems the bombshell claim is this:
"In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations."
So these authors seem to be claiming that OpenAI has not really proven Navier-Stokes at all. If I get their idea correctly, they are claiming that the LLM has not formalized the original "natural language" idea of Navier-Stokes correctly. If true, it would mean that their purported Lean proof is not actually a proof of Navier-Stokes at all, but something that is an incorrect translation of the original natural language idea. If correct, this is a really bold claim and I would like to see if other researchers agree.