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

21–30 of 136 posts

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

#21

Post by andrewchambers »

QwenGlazer9000 wrote: post #17
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?

It's because anthropic vibemathed it. I forgot the name but some other guy is working on a handwritten version of it and I bet it'll be more than just 1 magnitude faster.

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 .

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

#22

Post by calebkaiser »

redox99 wrote: post #12
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?

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 point: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...

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

#23

Post by returningfory2 »

lordnacho wrote: post #14

How do you know that it's formalizing what you think it's formalizing? If your Lean 4 has a bug, won't you be proving something other than what you thought?

Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

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

#24

Post by [deleted] »

btown wrote: post #15
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.

Heck, it’s even astonishing that any sort of generalized computer program could even verify a proof of this magnitude that hasn’t already been codified in a formal verification language. If, and it’s unclear that we’ll ever get the full story, they did draw inspiration from training on (or even directly accessing) rough notes that had been provided by another researcher in prose… the fact that it could leap so rapidl…

[deleted]

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

#25

Post by dooglius »

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.

I mean, I have a bachelor's in math and I don't imagine I could begin to understand either the human or LLM proofs without a massive investment of time and effort.

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

#26

Post by ramesh31 »

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.

>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 think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to master. It's going to be completely impossible for them to even remotely understand what that was like. Sort of like the pre-electricity days for us, but even more-so.

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

#27

Post by bethekidyouwant »

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..

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

#28

Post by advisedwang »

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?

But what hardware was the verification vs agents on? Because you are likely comparing verification on a single beefy machine (say XX TFLOPS total) to agents running on a substantial inference cluster (say XXXX TFLOPS). So you're 1 order of magnitude might actually be 2-4 orders of magnitude.

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

#29

Post by bethekidyouwant »

QwenGlazer9000 wrote: post #19
AndrewKemendo wrote: post #8

People are exhausted from being told/shown the thing they thought was special or unique or could make them relevant, is another mechanical puzzle that can be solved without joy. I don’t see that doing anything but intensifying in the short term

> But you see, now you'll have more time for the actual important things! > Like what? > Cleaning shit out of clogged toilets!

How about figuring out how to turn all of our shit into usable fertilizer?

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

#30

Post by sho_hn »

ramesh31 wrote: post #26
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.

>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 think about this a lot. I'll have to explain to my kids some day that there was long period of time where you couldn't just talk to a computer and have it talk back to you, and that communicating with one required special skills that took years of study to mast…

You're assuming you'll be the one doing the explaining :-)

It might also be that they won't even ask or wonder, similar to how most don't really do with pre-machining skills.

Or it could be like our "How did they build the Great Pyramid?!"

Post reply on HN