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–146 of 146 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 "WholeDomainPhysicalDomainTheorem.lean").

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

?

Post reply on HN