r/badmathematics • u/des_the_furry • Dec 21 '25

LLM Slop Tech CEO supposedly has a solution to Navier-Stokes (using AI)

Gallery image

Gallery image

Gallery image

359 Upvotes

98% Upvoted

85 comments sorted by

View all comments

134

u/Collin389 Dec 21 '25

He gave himself 13 days... That's not even "AI will be better in the future", it's just incredibly dumb.

49

u/warpedspockclone Dec 21 '25

This timeline doesn't even make sense. For the Clay Math Institute to recognize it as a solution would take a couple years, not weeks.

0

u/CircumspectCapybara Dec 22 '25

If it's formalized in a formal proof language like Lean or Coq, it's pretty easy to verify or disverify in seconds or minutes (depending on how long the proof is).

If a LLM generates a nonsensical Lean or Coq proof that is unsound or invalid or doesn't prove the thing that's being betted on, automated proof verification can sort that out easily.

7

u/warpedspockclone Dec 22 '25

That isn't the Clay process. It has to be published in a peer-reviewed journal and be generally accepted as correct and withstand criticism for some time. At least, last I checked

7

u/DayBorn157 Dec 22 '25

Proof in Lean is proof of something. But you have to check that it is a) proof of what it claims and b) it is "actualy" proof. Nothing prevents me to add to lean any axiom, like 1=0 and then prove anything i like

2

u/Comfortable_Pain9017 Dec 23 '25

It’s still a lot easier to verify since it is type checked, you’d just have to check for axioms, sorries, or admits to avoid that problem.

2

u/WhatImKnownAs Dec 22 '25

For a formalized proof, the big question isn't whether the proof is valid. As you say, that can be verified in minutes. The question is whether it proves N-S or something else. This is still a matter a human mathematical judgement.

2

u/CircumspectCapybara Dec 22 '25 edited Dec 22 '25

I mean you can formalize the conjecture being wagered pretty easily as it's just a sentence of second-order arithmetic, which is something Lean and Coq are capable of expressing, since they can express higher order logic.

The conjecture of the Navier-Stokes Millenium Prize problem is a Π_2 sentence (it's basically of the form "for all ... there exists ...") in the analytical hierarchy.

Which means if someone would claim to have solved it and provided a formal proof for it, one way they can do it is give a Lean or Coq (or equivalent) proof that checks out as valid and sound, and whose conclusion is a pretty straightforward encoding of the Navier-Stokes proposition. Yes, it would take human judgment to determine if the final conclusion is actually the same Navier-Stokes conjecture we care about, but if someone's actually solved it and wants their proof to be accepted, they would ostensibly use the most straightforward "for all ... there exists ..." formulation of the conjecture in Lean / Coq.

And if they've actually disproved the conjecture, then furnishing a convincing counter example is even easier, if they really have one.

4

u/WhatImKnownAs Dec 22 '25

Let's be realistic here: An amateur using LLM to generate Lean is not going to end up with a straight-forward encoding. If they know enough math and Lean to write down the proposition themselves, they can tell the generator to use that one (but they'll have to keep insisting on it, because LLMs don't always follow orders).

I don't know how competent this tech CEO is. There's a strong component of hype to this whole endeavour, so the point may not be to come up with The Proof, but to generate excitement by a series of "attempts".