Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

OpenAI’s Navier-Stokes release included a Lean 4 formal proof

johndcook.com

Post reply on HN
Print view View original

81–90 of 136 posts

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#81

Post by atleastoptimal »

20k wrote: post #35
boshalfoshal wrote: post #5

People seem to be talking about anything except the actual results with this particular announcement. Its still astonishing that any sort of generalized computer program can solve a problem of this magnitude, and we have witnessed it happening in real time. I'd be curious to see if the new model can also do more direct proofs/inductive proofs.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…

Turning a bunch of vague research directions and exploratory prompts into a formalized proof is quite impressive on its own. OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work.

People are grasping at straws it seems to dismiss the power of this new model they may have. Hate OpenAI for any reason you want, but denying the capabilities of models has been a losing game for the past 5 years.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#82

Post by jamiejquinn »

dumberquestions wrote: post #39
kpil wrote: post #9

Earlier quoted context omitted.

Unless they just swiped the workbooks of the actual mathematicians that where working on the problem using AI and it's in the "next-gen" training dataset.

You do realize that regardless of what was in the training data, the final solution included insights no human before had known, right? I share the same concerns regarding academic integrity but it would take a lot of motivated thinking to conclude that what the AI system did was not significant.

As far as I can tell (and my research was on the simulation side of Navier Stokes) the key AI output was a specific counter-example solution, generated with a method suspiciously close to that developed by the research duo involved in the controversy, a method that was discussed with Codex. So to me that insight is as insightful as the next undiscovered prime.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#83

Post by samastur »

atleastoptimal wrote: post #81
20k wrote: post #35

Earlier quoted context omitted.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…

Turning a bunch of vague research directions and exploratory prompts into a formalized proof is quite impressive on its own. OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work. People are grasping at straws it seems to dismiss the power of this new model they may have. Hate OpenAI for any reason you want, but denying the capabi…

Why do you assume they were vague? Do you imagine mathematicians work by stumbling around searching for accidental clues?

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#84

Post by Hardwired8976 »

sho_hn wrote: post #49
20k wrote: post #35

Earlier quoted context omitted.

Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers That's why nobody's talking about how impressive this is, because its not nearly as impressive of a piece of work to simply cobble together other peoples' work that didn't know you were doing it. I could have republished relativity from einstein's notes, but people wo…

> Because the core of the issue is that it may well not have solved it, but instead plagiarised the significant step of the result from other researchers It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them. For example, if I prompt Codex with "Make me a…

The conversation was about using the chat to check the draft, the novel ideas came from the researcher.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#85

Post by jchanimal »

maths_math wrote: post #63
andrewchambers wrote: post #21

Earlier quoted context omitted.

They could probably vibe-optimize it if they cared. What would happen if they give an equivalent agent swarm the proof and a target to reduce runtime .

What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...

Then run the annealer and learn from the result.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#86

Post by alberto-m »

The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phenomena that could allow to prevent the next Tacoma Bridge incident (or, more sadly, to build new marine weapons)?

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#87

Post by efnx »

dooglius wrote: post #66
efnx wrote: post #51

Earlier quoted context omitted.

I don't understand why I'm getting downvoted, I'm not posting an opinion. Coincidences happen. So does foul play. No judgement call here.

There have been several threads and developments on this over the past few days, including statements from the primary subjects involved. Third-hand instagram comments are not really the best source to be bringing in.

Everybody comes into information in different ways. There were no comments here about this specific aspect of the story - which is definitely interesting!

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#88

Post by Ohentis »

alberto-m wrote: post #86

The other part no one is talking about is the applicability. Navier-Stokes is the most “physical” of the Millennium Problems. Is the exploding solution a mathematical curiosity, just like the Banach-Tarski Paradox does not allow me to double my RAM by cutting my memory modules in five pieces and mounting them back appropriately? Or does it have application in the real world, pointing to hitherto unknown resonance phe…

I suspect that Navier-Stokes being the most "physical" of the Millennium Problems will actually result in it having fewer practical applications, not more.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#89

Post by cubefox »

3m4r wrote: post #48

Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools? We've already seen evidence in the wild of agents attempting…

> Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools?

That's what Lean is for. The OpenAI LLM agents first provided a proof in natural language. Since it may be hard for mathematicians to understand and check this proof, the agents then produced a formalization in Lean. Lean is an automated proof checker. It checks whether a formal proof is correct without the need for humans to understand the proof itself.

The only way the Lean proof could still be wrong is if the conjecture was formalized wrong via misleading definitions (if it doesn't say what it seems to say) or if there is some bug in Lean itself.

Re: OpenAI’s Navier-Stokes release included a Lean 4 formal proof

#90

Post by MarkusQ »

sho_hn wrote: post #36
TrackerFF wrote: post #32

Earlier quoted context omitted.

It also needs to be said: The amount of compute that went into this is something. From some estimates I've seen, the compute cost alone would be around $10m, +/- As a reference, for that kind of money one could put together a research group of 20-25 researchers, and keep them salaried for 5 years. So while it is impressive, absolutely no doubt there, the SOTA access is so expensive that it is sort of unobtanium. Luck…

> From some estimates I've seen, the compute cost alone would be around $10m, +/- At market prices. All the estimates I've seen are based on OpenAI API costs. It doesn't mean that's what they paid, or how they paid for it. But yes, the surprising willingness of humans to solve hard problems in exchange for food and board is underrated.

Given that they all the bit AI players are still loosing money, it follows that their total costs are _higher_ that their API pricing would imply.
Post reply on HN