9 comments

  • v64 8 hours ago
    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 [2]

    [1] https://x.com/AndrewCurran_/status/2096062392442724805 for example

    [2] https://en.wikipedia.org/wiki/Navier%E2%80%93Stokes_existenc...

    • cacio-e-pepe 7 hours ago
    • strangescript 3 hours 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 50 minutes 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.

    • hodgehog11 3 hours 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.
      • levocardia 22 minutes ago
        Anthropic sent out its Fermat's Last Theorem result to an expert on formalizing Fermat's Last Theorem in Lean, for what that's worth.
      • lumost 2 hours ago
        How do you know the lean is correct? You don’t bet the two trillion dollar company on “the ai said so”
        • adrianN 1 hour ago
          You carefully check that the problem is formalized correctly and then trust the Lean machinery to check the proof.
          • hodgehog11 1 hour 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.
        • krainboltgreene 1 hour ago
          I feel like that's exactly what's happened.
    • CSMastermind 8 hours 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.
    • bee_rider 8 hours 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.
    • bobmarleybiceps 5 hours ago
      if there's anything that would convince that LLMS are one of the biggest innovations ever, it would be this :-D
    • bilsbie 8 hours ago
      If it is solved what are the applications of that? What changes?
      • margorczynski 7 hours 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 2 hours 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 1 hour 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.
      • fatcatsbestcats 7 hours ago
        [dead]
  • goldenarm 8 hours ago
    @dang please can we add a [2014] to the title ?
    • thomasahle 8 hours ago
      Yes please. For a moment I thought Terrence Tao had scooped Anthropic.
  • tacomonstrous 8 hours ago
    This is essentially irrelevant to the content of the post, but it's amusing to me that he casually mentions submitting to JAMS as if its acceptance were a mere formality.
    • hodgehog11 3 hours ago
      It basically is a formality at this level. Many top math researchers now hardly even submit to journals at all and just put up a preprint.

      At this scale, peer review happens by the audience. They don't need a journal to get people reviewing their work.

    • gus_massa 7 hours ago
      • Sharlin 6 hours ago
        > With hindsight, some of my past rejections have become amusing. With a coauthor, I once almost solved a conjecture, establishing the result with an "epsilon loss" in a key parameter. We submitted to a highly reputable journal, but it was rejected on the grounds that it did not resolve the full conjecture. So we submitted elsewhere, and the paper was accepted.

        > The following year, we managed to finally prove the full conjecture without the epsilon loss, and decided to try submitting to the highly reputable journal again. This time, the paper was rejected for only being an epsilon improvement over the previous literature!

  • MeteorMarc 7 hours ago
    See https://www.quantamagazine.org/theory-of-fluids-enters-the-2... if you want to know what the Navier Stokes equations are about.
  • immmmmm 7 hours ago
    It’s pretty crazy what dynamics you get from NS.. until one realise they emerge from a tiny part of the solution space of Einstein equations.. which themselves emerge at the low energy limit of sth much bigger.
    • amluto 1 hour ago
      Can you actually credibly find NS or even Euler’s equations as an effective theory from GR?

      Euler’s equations and NS have this pesky velocity field, which requires the fluid’s state to be well described by a velocity at each point in space (and a density and a pressure, but I think GR has no problem with those). This means that you need some kind of interaction between particles to get them to exchange energy so that they thermalize instead of staying in the collisionless regime. (In other words, if you have two blobs of fluid collide, you need them to not go right through each other.) And I don’t think that GR is dissipating on the relevant scales.

      As a real-world example, the universe contains neat structures (the horsehead nebula is a somewhat famous example) that are consistent with dark matter distributions that don’t really resemble fluids.

    • cacio-e-pepe 7 hours ago
      Could you expand? Curious.
  • amelius 7 hours ago
    Interesting to see that they are not using the coordinate-free representation (exterior calculus, differential forms) that mathematical physicists prefer to use today.
    • auntienomen 6 hours ago
      Those notations are used when writing down the models, because they make clear the intrinsic geometry, the basic symmetries, etc. But they're not used so much in the study of solutions to the equations. Solutions tend to have peculiar features, tend to break underlying symmetries, etc. and there only needs to be one nasty particular solution to prove the NS conjecture wrong.
  • tug2024 40 minutes ago
    [dead]