OpenAI’s Navier-Stokes release included a Lean 4 formal proof • Hacker News Board

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

#141

Post by 20k » Fri, Sep 11, 2026, 1:21 AM UTC

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 » Fri, Sep 11, 2026, 1:24 AM UTC

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 » Fri, Sep 11, 2026, 1:34 AM UTC

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 » Fri, Sep 11, 2026, 1:35 AM UTC

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 » Fri, Sep 11, 2026, 1:40 AM UTC

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.