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

11–20 of 139 posts

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

#11

Post by sho_hn »

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.

> People seem to be talking about anything except the actual results with this particular announcement.

To be fair, most people have a fairly good handle on "Does opting out my prompts from training runs actually work?", but not on Navier-Stokes. They discuss what more immediately affects them.

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

#12

Post by redox99 »

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?

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

#13

Post by andrewchambers »

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?

If they aren't already, or if its possible, prove that an optimized version matches the simple version...

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

#15

Post by btown »

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 rapidly to a full formal verifiable Lean program for the entire scope of the problem is an incredible result in its own right.

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

#16

Post by gcgbarbosa »

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?

Maybe, but how many centuries would it take to prove it?

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

#17

Post by QwenGlazer9000 »

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.

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

#18

Post by Jblx2 »

pkal wrote: post #4

IMO the "forty hours per page" rule is not up to date, and more a consequence of lacking proof automation in 2005. From what I understand about Lean, this has been one of the things that they have put a lot of effort into improving, making proof mechanization more palatable to the mathematically inclined, as opposed to just logicians.

What is your estimate for the number of hours to formalize one page of undergraduate mathematics? Maybe you are saying this is close to zero, if/when Mathlib eventually covers all of undergraduate math?

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

#19

Post by QwenGlazer9000 »

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!

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

#20

Post by dist-epoch »

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?

Nobody wrote 13 mil lines proofs before.

I'm pretty sure you can make Lean at least 10 times faster if you unleash the agents on it.

Somebody ported Doom to run entirely in the TypeScript TYPES (not code). It took 12 days to compile.

https://www.tomshardware.com/video-games/porting-doom-to-typ...

Post reply on HN