Live data from Hacker News

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

161–162 of 162 posts

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

#161

Post by Ohentis » Fri, Sep 11, 2026, 4:05 AM UTC

davesque wrote: post #80

Regarding automatic formalization of proofs using AI, how do we know the formalization doesn't contain errors?

It depends on what you mean by that. In general we hope that the environment and theorum statements are correct. If they are, we know that the formal proof proves the theorum we want. If your asking how we know that the formal proof actually matches the informal proof, we do not.

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

#162

Post by Ohentis » Fri, Sep 11, 2026, 4:26 AM UTC

jasonfarnon wrote: post #133

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.

That sounds like PR nonsense to me. These companies have had teams of mathematicians for at least 1.5 years looking to make headlines, and they didn't bother trying all 10 millennium problems? Yeah right.

I mean they might not have tried spending 30 million dollars with a new model yet.

Post reply on HN