[hodgehog11]

Something else to add is mathematical discovery. There is a team that is very close to solving the Navier-Stokes Millenium Prize problem: https://deepmind.google/discover/blog/discovering-new-soluti...

The cynists will comment that I've just been sucked in by the PR. However, I know this team and have been using these techniques for other problems. I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point. If they don't do it, I'm pretty sure I could take a handful of people and a few years and do it myself. Mostly a lot of interval arithmetic with a final application of Schauder that remains; tedious and time-consuming, but not overly challenging compared to the parts already done.

[PontifexCipher]

This is not just PR and is very interesting. However, in my view, (and from a quick read of the paper) this is actually a very classical method in applied math work:

- Build a complex intractable mathematical model (here, Navier-Stokes)

- Approximate it with a function approximator (here, a Physics Informed Neural Network)

- Use the some property of function approximator to search for more solutions to the original model (here, using Gauss-Newton)

In a sense, this is actually just the process of model-based science anyway: use a model for the physical world and exploit the mathematics of the model for real-world effects.

This is very very good work, but this heritage goes back to polynomial approximation even from Taylor series, and has been the foundation of engineering for literal centuries. Throughout history, the approximator keeps getting better and better and hungrier and hungrier for data (Taylor series, Chebyshev + other orthogonal bases for polynomials, neural networks, RNNs, LSTMs, PINNs, <the future>).

You didn't say anything to the contrary, and neither did the original video, but it's very different than what some other people are talking about in this thread ("run an LLM in a loop to do science the way a person does it"). Maybe I'm just ranting at the overloading of the term AI to mean "anything on a GPU".

[hodgehog11]

This is absolutely true, but it still makes use of the advantages and biases of neural networks in a clever way. It has to, because computationally-assisted proofs for PDEs with singularities is incredibly difficult. To me, this is not too similar from using them as heuristics to find counterexamples, or other approaches where the implicit biases pay off. I think we do ourselves a disservice to say that "LLMs replacing people" = "applications of AI in science".

I also wouldn't say this is entirely "classical". Old, yes, but still unfamiliar and controversial to a surprising number of people. But I get your point :-).

[nybsjytm]

> I know they are so close to a computationally-assisted proof of counterexample that it is virtually inevitable at this point.

That's a strong claim. Is it based on more than the linked work on some model problems from fluid mechanics?

I will say that I dread the discourse if it works out, since I don't believe enough people will understand that using a PINN to get new solutions of differential equations has substantially no similarity to asking ChatGPT (or AlphaProof etc) for a proof of a conjecture. And there'll be a lot of people trying to hide the difference.

[hodgehog11]

It's based on knowledge of the related estimates, applying similar techniques to geometric problems, knowledge of all the prior works that lead to the current work, and speaking with members of the team themselves. They are much further along than it appears at first glance. All of the major bottlenecks have fallen; the only concern was whether double precision accuracy is good enough. The team seems to have estimates that are strong enough for this, but obviously keep them close to their chest.

PINNs are different in concept, yes, but clearly no less important, so the additional attention will be appreciated. Asking LLMs for proofs is a different vein of research, often involving Lean. It is much further behind, but still making ground.

[nybsjytm]

> PINNs are different in concept, yes, but clearly no less important

If anything I think they're more important! Whether or not it works out for Navier-Stokes, this kind of thing is an extremely plausible avenue of approach and could yield interesting singularities for other major equations. I am however extremely concerned about public understanding. I know you are well aware that this is worlds away from the speculative technologies like 'mathematical superintelligence' but, if it works out, it'll be like a nuclear bomb of misinformation about AI and math.

[11101010001100]

I think the PR is making it seem that Deepmind is not standing on the shoulder of giants, when in fact it very much is. The paper itself makes this clear. I wish them luck!

[hodgehog11]

To add to this, I think it is important to recognise that this is not fundamentally a Deepmind project; engineers from Deepmind came to help with the computational aspects to bring the error down after the lead and last authors brilliantly realised this approach would work with a proof of concept back in 2023. A good amount of work from Deepmind was involved, but I don't like the idea that they could get all the credit for this.

[nybsjytm]

> brilliantly realised

Can you say more about this? Nothing about this approach seems very amazing to me. Construct an approximate solution by some numerical method (in this case neural networks), prove that a solution which is close enough to satisfying the equation can be perturbed to an exact solution. Does the second half use some nonstandard method?

[hodgehog11]

This is one of those things that seems easy in retrospect, but wasn't particularly obvious at the time.

1. Proving existence to a differential equation using a numerical approximation is quite a bit more difficult than it seems at first. For Euler or NS, it seems almost absurd. Not only do you need a rather substantial amount of control over the linearisation, you need a way to rigorously control a posteriori error. This is easy for polynomials, but doing it for other models requires serious techniques that have only been created recently (rigorous quadrature via interval arithmetic).

2. Further to that, neural networks are far from an obvious choice. They are not exactly integrable and it is certainly not clear a priori that their biases would help to search for a blowup solution. In fact, I would have initially said it was a poor choice for the task. You also need to get it to a certain degree of precision and that's not easy.

3. The parameterisation of the self-similar solution turns out to be completely appropriate for a neural network. To be fair, solutions of this type have been considered before, so I'm willing to chalk this down to luck.

It's difficult to explain how challenging it is to fully derive a plan for a computationally-assisted proof of this magnitude unless you've tried it yourself on a new problem. At the end it seems completely obvious, but only after exhausting countless dead ends first.

[TZubiri]

Worth noting that deep mind is a world class pre-LLM team. And the techniques used are completely unrelated to LLMs

[rossant]

They are building a formally-defined counter example to this? Am I understanding correctly?

> In three space dimensions and time, given an initial velocity field, there exists a vector velocity and a scalar pressure field, which are both smooth and globally defined, that solve the Navier–Stokes equations.

[hodgehog11]

They find a very good approximate blowup solution (non-smooth) using a NN. When the solution is good enough, you just need careful fixed point theory to infer an actual solution.

[mlpoknbji]

If it was a sure thing, why publish the paper they did? Why not just solve NS?

[hodgehog11]

It will take another few months at least, and the rest of the argument will comprise a fair few pages. But the hardest part is over.

When working toward a problem of this magnitude, it is natural to release papers stepwise to report progress toward the solution. Perelman did the same for the Poincare conjecture. Folks knew the problem was near a solution once the monotonicity proof of the W functional came out.

[nybsjytm]

> Folks knew the problem was near a solution once the monotonicity proof of the W functional came out.

This isn't true, it was a major accomplishment but by far the easiest part of Perelman's papers and not actually even part of the proof of the Poincaré conjecture.

[hodgehog11]

Interesting, this was the big 'a-ha' moment in the grad course I took on the subject. Surgery was clearly important too, but this seemed to be more apparent from Hamilton's work. The W functional was what provided the control needed. Also, calling it 'easy' feels like it dismisses the insights necessary to have developed the functional in the first place.

Happy to be corrected on this; I wasn't an active mathematician at the time, so everything I know comes from other accounts.

[nybsjytm]

I called it the easiest part of his papers, not easy. Either way, it's actually not relevant to the proof. For example, I believe that Morgan and Tian's 500 page exposition of the proof doesn't mention it even once.

Moreover I'd strongly dispute that there was any particular point where it was clear that the problem was "near a solution." The W functional is an example where experts could very quickly verify that Perelman had made at least one major new discovery about the Ricci flow. But the proof of the Poincaré conjecture was on another order of complexity and required different (more complicated) new results about Ricci flow.

[Fraterkes]

What would the implications of solving NS actually be? Would we get much more accurate weather predictions?

[geordiew]

I think it is fair to say that any blowing-up solution of navier stokes would be of purely intellectual interest. NS is a problem that many smart people have thought about and failed to solve. The current picture is that there are probably self-similar blowing up solutions that exist at extremely high codimension in the space of initial conditions. Thus they are "probability zero", and, if essentially never arise in nature. (A nice analogy: imagine a movie of a stone falling into a pond, and the ripples created afterwards. Now run the movie of the ripples backwards. We never see this in nature!)

[ants_everywhere]

> The cynists will comment that I've just been sucked in by the PR

You can just ignore them. I see a lot of science-literate folks try to meet the anti-science folks as if they're on equal footing and it's almost always a waste of time. Imagine if every time you talked about biology you had to try to address the young earth creationists in the room and try to pre-rebut their concerns.