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

141–150 of 159 posts

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

#141

Post by 20k »

manofmanysmiles wrote: post #118
atleastoptimal wrote: post #81

Earlier quoted context omitted.

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…

> OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work. I'm not sure I follow, considering the waterfall of evidence of unethical behavior flowing from OpenAI. A few major ones: - Safety team departures and dissolution in 2023 and 2024 - Mass copyright infrigement lawsuits - Scarlett Johansson Voice Controversy - For-Profit Conve…

Especially after they committed textbook misconduct by trying to purge one of the paper authors because he worked for a competitor

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

#142

Post by jazzyjackson »

bethekidyouwant wrote: post #27
efnx wrote: post #10

I heard a rumor (on instagram, so YMMV) that the professor who was closest to solving this problem had only weeks ago used Codex, which had slurped up all his notes on the subject. Now OpenAI's agents solve the problem. If it's true that seems like quite a coincidence.

How could they possibly included in the previous training run which takes months to complete..

Has it not been the usual process to snapshot a model to use for inference while continuing to run the training process? I guess you can’t add to the training corpus once you begin? Just trying to make sense of whether training begins or ends as rigidly as you suggest.

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

#143

Post by symfoniq »

jcalx wrote: post #128
stabbles wrote: post #7

It's kinda funny to realize that Lean is apparently so slow that for Fermat's Last Theorem proof verification runs only 1 order of magnitude faster than agents could generate the Lean code (15h verification with 230GB of RAM vs 11 days to generate it). To what extent can you optimize Lean? It has to be simple enough to be auditable, does that mean you cannot use opaque optimizations to make it run faster?

> 230 GB of RAM "I have discovered a truly marvelous proof of this, which my memory is too small to contain..."

They’re using Electron to write proofs now?

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

#144

Post by symfoniq »

manofmanysmiles wrote: post #118
atleastoptimal wrote: post #81

Earlier quoted context omitted.

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…

> OpenAI would have no incentive to taint its first math announcement of this magnitude if it knew it were "plagiarizing" another person's work. I'm not sure I follow, considering the waterfall of evidence of unethical behavior flowing from OpenAI. A few major ones: - Safety team departures and dissolution in 2023 and 2024 - Mass copyright infrigement lawsuits - Scarlett Johansson Voice Controversy - For-Profit Conve…

Ye shall know them by their fruits.

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

#145

Post by bethekidyouwant »

s900mhz wrote: post #37
bethekidyouwant wrote: post #27

Earlier quoted context omitted.

How could they possibly included in the previous training run which takes months to complete..

IMO It’s not about being trained on the data, it’s more like what do the agents have access to during inference? Can they grep customer transcripts/logs?

You’re saying that when they we’re trying to solve this theorem they also shoved in its context somebody else’s chat logs? Bruh.

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

#146

Post by Jblx2 »

davesque wrote: post #80

Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?

In a similar vein, where does the theorem statement even reside, just so we can take a look at how large that is? Is it the four files with "Theorem" (and no "Comparator") in the file name? ("R3/Theorem.lean", "LocalPaperTheorem.lean", "PeriodiocPaperTheorem.lean", and "WholeDomainPhysicalStageTheorem.lean").

https://github.com/openai/NavierStokesAndEuler/blob/main/Nav...

?

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

#147

Post by jgalt212 »

I found this bit interesting.

> Even so, an error in the theorem prover does not mean an error in the original result. For an incorrect result to slip through, the AI-generated proof would have to be wrong in a way that happens to exploit an unknown error in the theorem prover. It is far more likely that you’re trying to prove the wrong thing than that the theorem prover let you down.

AIs are known to cheat. Given such, they would surely exploit such a bug if they found one.

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

#148

Post by magicalist »

tristanj wrote: post #136
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…

It is very unlikely to be plagiarized, and claims of plagiarism are largely unfounded and show a lack of understanding of the situation. They fall apart when reviewing the timeline, and what was actually solved. This is the timeline: On June 29, Buckmaster opted out of model training, and stopped allowing his chats to be used as training data with OpenAI https://mastodon.social/@tristanbuckmaster/11723341370570119...…

> And OpenAI directly addressed these plagiarism claims, and called them impossible

Funny, you were telling me two days ago that on the contrary, "it’s genuinely impossible to know how much of Buckmaster’s Codex data is in OpenAI’s training set":

https://news.ycombinator.com/item?id=49621648

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

#149

Post by btilly »

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…

The other researchers themselves were also using AI. That's why it was potentially available to be plagiarized.

There is no human only proof of this.

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

#150

Post by felipeerias »

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…

It's perfectly reasonable to assume that the result itself is legit and that OpenAI behaved unethically.

Even by their own account, they decided to throw an unpublished model and millions of dollars in compute at this particular problem simply because they had heard rumours that other people were making progress and wanted to snatch the prize from them.

Post reply on HN