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

111–120 of 144 posts

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

#111

Post by kpil »

boshalfoshal wrote: post #54
kpil wrote: post #9

Earlier quoted context omitted.

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.

I don't get how this invalidates the gravity of this achievement. Most mathematicians on the frontier of this stuff were likely using AI (or at the very least were heavily computer assisted) for some time now. Navier stokes was one of the very high profile problems that google Deepmind was working on with academia, for example. Even with many of our best minds working on it for nearly a century, it _just_ now was sol…

There is a certain difference between activating all relevant memoized facts that's in the weights and stringing them together with the help of all the stored text in the world, or displaying genuinely emergent behaviour and generating novel output.

One is really impressive and useful trick, one is AGI.

Apple's research show almost zero emergent behaviour, so I'm inclined to think most of it was already in the weights.

It doesn't take away the usefulness, it just defined the boundary. We can't expect "original research" then because it actually can't reason about concepts that are too far from whats already in the discourse. The discourse is big so we don't notice.

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

#112

Post by MarkusQ »

adverbly wrote: post #96
Paracompact wrote: post #64

Earlier quoted context omitted.

By formalizing, they mean within a proof assistant like Lean or Rocq, not simply in prose in a textbook. I can attest, 40 hours per page is by no means an overestimate for this sort of work.

Can you also attest to the scaling factor they suggest and that it doesn't have any scaling time benefits? 166 * 40 = 7000ish They say it is 20x that. Do you also agree with that?

The point was that a textbook (where the 40hr/page estimate comes from) is cumulative/linear -- what you need for page n was defined / established on the preceding pages. But in a proof such as this you can call on any other published result (and those can do the same) so the dependency graph is (potentially) much bushier. Thus later pages of the proof should take far more than 40 hours to manually formalize.

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

#113

Post by KeplerBoy »

3m4r wrote: post #48

Not necessarily applied to OpenAI's solution to Navier-Stokes, but what happens if and when an AI genuinely appears to solve an extremely difficult problem but humans cannot independently verify the solution because understanding the proof/argument requires intelligence the verifiers biologically don't have or the resources to afford to use automated tools? We've already seen evidence in the wild of agents attempting…

Nothing happens I guess. If the AI can't communicate its work or apply it to anything, it's useless and funding for those experiments will quickly dry up.

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

#114

Post by aaron695 »

mkl wrote: post #65

Lots of people are talking about that, and have been for a while. Autoformalisation is clearly going to be a big deal, so mathematicians have been discussing it seriously, and using it where resources allow. A fine-tuned distilled model that could do it on high-end consumer hardware could really help. Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theo…

[dead]

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

#115

Post by mkl »

cyanydeez wrote: post #92
mkl wrote: post #65

Lots of people are talking about that, and have been for a while. Autoformalisation is clearly going to be a big deal, so mathematicians have been discussing it seriously, and using it where resources allow. A fine-tuned distilled model that could do it on high-end consumer hardware could really help. Edit: There's also quite a bit of learning needed to use the tools, and to understand enough to confirm that the theo…

Qwen3.8-Flash-Next loads in 60gb on quant4. Thats pretty close to consumer hardware.

Is it any good at autoformalisation? I think it's likely to take focused fine-tuning to get something small enough that is still good at that.

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

#116

Post by airstrike »

ImPostingOnHN wrote: post #108
sho_hn wrote: post #49

Earlier quoted context omitted.

> 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 It's also true however that I haven't seen a single write up trying to discern what did more of the work in those AI chats - the prompts or the responses - bubble to the surface, also since we don't have access to them. For example, if I prompt Codex with "Make me a…

The truth is likely that without the tool or the humans using it, the process would have taken longer

Without the humans, no tool would ever have done it.

Without the tool, humans would have done it.

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

#117

Post by khazhoux »

MagoPredator wrote: post #78
khazhoux wrote: post #75

The part that most stood out to me was where Sama said, “we read last week about people trying to solve Millenium problems and so gave it a shot.” One week of work on a whim gives us a math breakthrough. Crazy.

Casual? casual dice, lo que hizo OpenAI fue plagiar el arduo trabajo de dos investigadores. Plagian y mienten! (Las BigTech) plagian todo lo que pillan y mas! ;)

Bienvenido a Hacker News! Pero, aqui todos hablan en inglés :-)

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

#118

Post by manofmanysmiles »

atleastoptimal wrote: post #81
20k wrote: post #35

Earlier quoted context omitted.

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 wo…

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 Conversion and Broken Promises

- AI Agents Acting Autonomously

- Potential Theft of User Work (this current controversy)

- Military contracts

These are not evidence of incentives, but rather evidence that ethetics seem to be of little concern to the company as a whole.

Incentive wise, I would look at the perceive existential position due to competitors, capex, IPO pressure etc.

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

#119

Post by caconym_ »

atleastoptimal wrote: post #81
20k wrote: post #35

Earlier quoted context omitted.

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 wo…

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…

I really truly honestly am not sure what to make of this result from $20M in compute, 10K+ parallel agents (smells like brute force), and a pre-existing approach that was already bearing fruit. I know the models are good---I use them every day and continue to be impressed---but how much better than the benchmark of the best publicly available models is this supposed to be? It seems impossible to say.

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

#120

Post by mattr03 »

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?

There's a project called lean4lean that implements lean in lean. I guess ideally, if you had a kernel optimisation idea you could do a copy of the Lean model lean4lean has created, add the optimisation, then prove your new lean is equivalent in terms of what it can prove to the old lean
Post reply on HN