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.
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.
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.
- 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".
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 :-).
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.
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?
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.
> 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.
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.
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.
Happy to be corrected on this; I wasn't an active mathematician at the time, so everything I know comes from other accounts.
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.
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.