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

61–70 of 127 posts

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

#61

Post by 20k »

sho_hn wrote: post #49
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…

> 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 researchers apparently spend a year or so working on this, and it builds off significant previous work, so it seems like it was a pretty significant amount of work that OpenAI may have trained on

I'd love to see an in depth analysis of how much OpenAI actually did, but I suspect we'll never see that because it would indicate at least some plagiarism which undermines a lot of what OpenAI is putting out in public

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

#62

Post by zamadatix »

huurtehoog wrote: post #52
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…

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.

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

#63

Post by maths_math »

andrewchambers wrote: post #21
QwenGlazer9000 wrote: post #17

Earlier quoted context omitted.

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 .

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

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

#64

Post by Paracompact »

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.

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

#65

Post by mkl »

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 theorem being verified is what you think. And of course a lot of maths can't yet be expressed in Lean as the foundations haven't been built up enough.

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

#66

Post by dooglius »

efnx wrote: post #51
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.

I don't understand why I'm getting downvoted, I'm not posting an opinion. Coincidences happen. So does foul play. No judgement call here.

There have been several threads and developments on this over the past few days, including statements from the primary subjects involved. Third-hand instagram comments are not really the best source to be bringing in.

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

#67

Post by jcranmer »

scuppernong wrote: post #50
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.

this is not a rumor (the allegation, anyway), it's reported in the new york times

Newspapers are not above printing rumors.

See, e.g., Barak Ravid regularly reporting in Axios the impending ceasefire negotiation progress in the Iran War, which largely have failed to come to pass.

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

#68

Post by mr-pink »

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.

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

#70

Post by [deleted] »

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…

[deleted]
Post reply on HN