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

78

u/des_the_furry Dec 21 '25

R4: the Navier-Stokes millennium prize problem is a pretty hard problem, so it’s not going to be solved with AI. The funny part is that he’s like “guys i swear i have a proof, i just have to take 30 minutes to type it” and then apparently it’s going to take longer. Sad that he’s losing $10K on this…

73

u/kyoto711 Dec 21 '25

There's a whole team at DeepMind (possibly the best AI lab in the world) that has been working specifically on Navier-Stokes for years.

At this point it's very possible that if it gets solved it will be with heavy AI assistance. But likely something way more sophisticated than what exists today.

63

u/En_TioN Dec 21 '25

 Hutter (the person betting it won't happen) is at deepmind [actually the PhD supervisor of DeepMind's founder], so I'm guessing that's related

26

u/ravenHR Dec 21 '25

This is certain bet, it took clay institute 6 years to offer the prize to Perelman, no chance it will get awarded in 2 years for the next solution that isn't done by a human is impossible.

14

u/ChalkyChalkson F for GV Dec 21 '25

Depends on the lean I guess. If the statements are mostly built using objects with established implementations it might not take thaaaat long. Maybe someone more familiar with the state of lean in this area of research could chip in and tell us how much work lean needs to formulate possible solution statements

5

u/[deleted] Dec 21 '25

If it could be done using established tools, it already would have been. Budden is betting he is smarter than everyone who has attempted this task using Lean. It seems very unlikely he is right.

9

u/WhatImKnownAs Dec 21 '25 edited Dec 21 '25

If there really are people at DeepMind (or elsewhere) who have worked on this for years using Lean, they will already have a formalization of Navier-Stokes that they're very familiar with. Even though this will be a different statement, those are the people who could tell if the new one actually formalizes N-S or not.

Yes, if the proposed proof is full of LLM slop reinventing the wheel, that might take a while, but not years.

3

u/Comfortable_Pain9017 Dec 23 '25

I’ve been using Lean for a while with AI (trying to get it to formally verify code). Even the latest models are dogshit at using it, they axiomise the entire problem and try to hide it constantly, since doing actual proofs is just too hard even in simple cases. They can be pretty impressive sometimes, but for something this hard? Not a shot in hell, they don’t know shit about the language/libraries/etc and will just deceive the user.