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

#91

Post by cubefox » Thu, Sep 10, 2026, 10:54 PM UTC

tecleandor wrote: post #58

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…

Well that happened already without AI to Mochizuki with his proposed solution to the abc conjecture.

So an LLM (or more realistically, a huge swarm of agents) should check his work, find a mistake or gap, or, if there is none, provide a formal verification.

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

#92

Post by cyanydeez » Thu, Sep 10, 2026, 10:55 PM UTC

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.

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

#93

Post by arjvik » Thu, Sep 10, 2026, 10:55 PM UTC

cubefox wrote: post #89

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…

> 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? That's what Lean is for. The OpenAI LLM agents first provi…

Sadly, as ideal as this seems, Lean has a history of kernel bugs that allow one to prove False.

It's unlikely to be the case here as instead of hillclimbing a Lean proof for validity it appears the proof was first constructed in English before being translated to Lean, which intuitively (hopefully) reduces the chance it exploits a bug.

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

#94

Post by andrewchambers » Thu, Sep 10, 2026, 10:55 PM UTC

maths_math wrote: post #63

andrewchambers wrote: post #21

Earlier quoted context omitted.

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 .

What would be the point of that though? I think the reason Kevin wants to optimize it is for the understanding that will result from the process, not because anyone cares about having a Lean proof that compiles quickly...

I was replying to the comment about it being slow to run. I wasn't commenting on understanding it.

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

#95

Post by bloppe » Thu, Sep 10, 2026, 10:55 PM UTC

mr-pink wrote: post #68

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…

you dont have to take headlines literally.

Most people do, so the literal interpretation matters a lot

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

#96

Post by adverbly » Thu, Sep 10, 2026, 10:56 PM UTC

Paracompact wrote: post #64

adverbly wrote: post #57

> formalizing the 166-page paper from OpenAI would take 132,800 person-hours Am I missing something or is this completely out of the ballpark? I must be missing something or the upvote bots are out in force for this one... If this were remotely true it would be impossible for anyone to write a math textbook.

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?

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

#97

Post by MarkusQ » Thu, Sep 10, 2026, 10:56 PM UTC

contravariant wrote: post #55

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.

In a way that works just as well but the incentives are messed up. And that's before we get into the whole 'salt the earth' way they ended up solving it. For a short period of time it may well have been the least valuable proof in mathematics yet. In their haste it's dubious they actually read the proof, and I don't think anyone has had time yet to truly understand it (the original researchers are best placed to do s…

This.

The point of these problems is the understanding / tooling gained in solving them. We're getting none of that. At best they are like a modern oracles, correctly answering your questions in a way that's doesn't help you any. (At worst,...)

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

#98

Post by huurtehoog » Thu, Sep 10, 2026, 10:57 PM UTC

zamadatix wrote: post #62

huurtehoog wrote: post #52

Earlier quoted context omitted.

That's true of the entirety of mathematics. Its validity is a social construct. That is not to relativize it entirely, but much of what was considered good and sound mathematics in the ancient Agean for example would now fall way short of what mathematicians consider valid proofs. Mathematics is a human endeavor funded on communicating and sharing mental constructs. Some are useful but most of it is not about produci…

There's a large difference between "wrong for the given definitions" and "right in that context, but wrong for other definitions" though.

I think I am make a much more basic point than what you're talking about but then again I am not sure what you're tying to say here...

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

#99

Post by aleph_minus_one » Thu, Sep 10, 2026, 10:58 PM UTC

kens wrote: post #47

It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis. A mathematician (Mochizuki) claimed to have proven it in 2012 using a new theory called "Inter-universal Teichmüller theory" that almost nobody understands. Some mathematicians think the proof is correct while the majority don't. So the conjecture is in this annoying limbo where its s…

> It would be nice if someone used AI and/or Lean to sort out the abc conjecture, an important unsolved problem in Diophantine analysis.

People did attempt this:

https://github.com/katobungen/LANA_report_202607/blob/pdf/LA...

Here are Kirti Joshi's comments about the LANA project report: https://bpb-us-e2.wpmucdn.com/sites.arizona.edu/dist/4/404/f...

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

#100

Post by Ohentis » Thu, Sep 10, 2026, 10:59 PM UTC

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?

The only places you can really have a bug are your theorum statement, your axioms, your environment (hardware, operating system, etc.), and the lean kernel itself. In most situations you don't have the AI control any of these. The only risk is the AI discovering and exploiting a bug in one of these systems instead of actually providing what you want to prove.