6 ms·

This is going around due to rumors and baseless speculation on Twitter [1] right now that Anthropic has solved the Millennium problem related to Navier-Stokes [

• CSMastermind 11d ago
  Lol as far as I know that post was the origin of that claim and it's clearly just a guy predicting something that will happen in the future with no information about it.
  • krackers 11d ago
    Elliot Glazer (FrontierMath lead) traces how it snowballed over time https://x.com/ElliotGlazer/status/2096298696438906934 https://x.com/ElliotGlazer/status/2096298696438906934
    • Arodex 11d ago
      Not reading any x.com content until xcancel and nitter are back.
      • nozzlegear 10d ago
        Yeah, can't read anything on xitter due to the gigantic dickover they put over the content when you don't have an account. A screenshot would've been more helpful than an xitter link.
      • sawjet 11d ago
        Dear diary...
        • deleted 10d ago
          [deleted]
      • perching_aix 11d ago
        here you go: https://nitter.kareem.one https://nitter.kareem.one
• bilsbie 11d ago
  If it is solved what are the applications of that? What changes?
  • fatcatsbestcats 11d ago
    [dead]
  • margorczynski 11d ago
    None really. It just says if the NS equations are realistic and can really model real physics or there exist some solutions that make it blow up (infinite energy). But even if that would exist (a solution that blows up) it doesn't mean it doesn't work for 99,999999% of the stuff we're interested in. The question is basically a pure math question about PDEs.
  • lumost 11d ago
    Maximally, a closed form solution would remove the need for Computational Fluid Dynamics. Any property could be derived from a (presumably expensive) analytic function. Minimally. It could say that no such analytic function can ever exist. Which would be rather boring. Turbulent fluids look awfully predictable with their spirals….
    • amluto 11d ago
      That would be surprising IMO. We have closed form solutions to Newton’s Laws plus gravity (albeit not very many of them), we have several closed form solutions to Einstein’s equation in GR, and we have a whole lot of closed form solutions to Maxwell’s equations. But we still use numerical methods to solve interesting problems in all of these fields.
  • neutrinobro 11d ago
    Honestly, for practical engineering purposes not that much. The Navier-Stokes equations are an approximation for a mathematically ideal in-compressible fluid. Even ignoring compressibility, physical fluids in the real world are not continuous fields since they are composed of discrete molecules. However, for that small class of problems where an analytic solution can be found, then it means you can be confident in the answer (it won't blow up to infinity), and that there are no other alternate solutions to the same problem.
• bee_rider 11d ago
  For a second I thought they were aiming the scary proof machine at us mortals doing PDE stuff. Fortunately the speculation is just that they happen to be aiming it at a nearby mathematician type problem. Phew.
• cacio-e-pepe 11d ago
  relevant: https://mathstodon.xyz/@tao/117219101339291693 https://mathstodon.xyz/@tao/117219101339291693
  • goldenarm 10d ago
    Key quote : "Solving the problem by purely AI-powered methods [would be a] net negative for the progress of mathematics."
• bobmarleybiceps 11d ago
  if there's anything that would convince that LLMS are one of the biggest innovations ever, it would be this :-D
• hodgehog11 11d ago
  Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
  • lumost 11d ago
    How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”
    • adrianN 11d ago
      You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.
      • hodgehog11 11d ago
        Exactly, and the advantage is that checking that the problem is "formalized" here is essentially isolated to verifying that the final theorem statement matches the claim. If there are no 'sorry's and the program compiles, then it has been proven. That's the point of Lean.
      • zarzavat 10d ago
        As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.
      • wiz21c 10d ago
        Each word of your answer is carefully chosen. I'll add one sentence though: you let time do its job. Of course there may be errors in lean, of course AI can take advantage of it, of course "carefully" is full of errors. So the only thing left is waiting to see if the result holds. And yes, it may take 30 years...
    • krainboltgreene 11d ago
• strangescript 11d ago
  This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
  • throwaway81523 11d ago
    There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that. Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it? Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.