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

#31

Post by dooglius » Thu, Sep 10, 2026, 10:09 PM UTC

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?

Weren't the agents massively parallel, whereas the lean verifier presumably is not? Also, I presume said agents were themselves running the verifier on their own parts many times.

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

#32

Post by TrackerFF » Thu, Sep 10, 2026, 10:10 PM UTC

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.

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.

Luckily, the prices have historically reduced by a factor of 5-10 every year...but still, only those that swim in cash can afford this.

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

#33

Post by Yizahi » Thu, Sep 10, 2026, 10:10 PM UTC

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.

Aren't you doing exactly the same thing as people you are mentioning? Skipping "talking about actual results" to talking about general capabilities of this LLM and computers in general? because that's exactly what seems like 99% of all people had been doing lately - debating what computer programs can do and what they can't.

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

#34

Post by stabbles » Thu, Sep 10, 2026, 10:11 PM UTC

calebkaiser wrote: post #22

redox99 wrote: post #12

Earlier quoted context omitted.

Can you use Lean to... prove "Lean-fast" is equivalent to Lean?

Yeah, in essence. This is actually a pretty cool part of working in Lean. It's a somewhat normal convention to write something in a human readable way and then write a second optimized implementation with some kindness of correctness theorem connecting them. There was a whole open "competition" for writing a faster Lean kernel/proof checker that didn't sacrifice on soundness called Lean Kernel Arena. Fun reference po…

Great read, thanks for sharing

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

#35

Post by 20k » Thu, Sep 10, 2026, 10:12 PM UTC

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 would correctly not be impressed with my ability

Until the plagiarism scandal is sorted out, its not a meaningful result at all, because nobody knows how much genuine innovation these models are displaying

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

#36

Post by sho_hn » Thu, Sep 10, 2026, 10:12 PM UTC

TrackerFF wrote: post #32

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.

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.

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

#37

Post by s900mhz » Thu, Sep 10, 2026, 10:12 PM 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..

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?

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

#38

Post by 1121redblackgo » Thu, Sep 10, 2026, 10:12 PM UTC

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.

See other thread, but yeah that's the general ballpark of the situation.

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

#39

Post by dumberquestions » Thu, Sep 10, 2026, 10:12 PM UTC

kpil wrote: post #9

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.

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.

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

#40

Post by mswphd » Thu, Sep 10, 2026, 10:12 PM 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..

I won't take a side in things, but OpenAI stated the model they used here started training August 28th. Note that "training" here might mean "post-training with RLHF an Astra base model" or something. but training had only started a little over a week earlier.