Computer Proof ‘Blows Up’ Centuries-Old Fluid Equations

For centuries, mathematicians have sought to understand and model the motion of fluids. The equations that describe how ripples crease the surface of a pond have also helped researchers to predict the weather, design better airplanes, and characterize how blood flows through the circulatory system. These equations are deceptively simple when written in the right mathematical language. However, their solutions are so complex that making sense of even basic questions about them can be prohibitively difficult.

Perhaps the oldest and most prominent of these equations, formulated by Leonhard Euler more than 250 years ago, describe the flow of an ideal, incompressible fluid: a fluid with no viscosity, or internal friction, that cannot be forced into a smaller volume. “Almost all nonlinear fluid equations are kind of derived from the Euler equations,” said Tarek Elgindi, a mathematician at Duke University. “They’re the first ones, you could say.”

Yet much remains unknown about the Euler equations — including whether they’re always an accurate model of ideal fluid flow. One of the central problems in fluid dynamics is to figure out if the equations ever fail, outputting nonsensical values that render them unable to predict a fluid’s future states.

Mathematicians have long suspected that there exist initial conditions that cause the equations to break down. But they haven’t been able to prove it.

In a preprint posted online last month, a pair of mathematicians has shown that a particular version of the Euler equations does indeed sometimes fail. The proof marks a major breakthrough — and while it doesn’t completely solve the problem for the more general version of the equations, it offers hope that such a solution is finally within reach. “It’s an amazing result,” said Tristan Buckmaster, a mathematician at the University of Maryland who was not involved in the work. “There are no results of its kind in the literature.”

There’s just one catch.

The 177-page proof — the result of a decade-long research program — makes significant use of computers. This arguably makes it difficult for other mathematicians to verify it. (In fact, they are still in the process of doing so, though many experts believe the new work will turn out to be correct.) It also forces them to reckon with philosophical questions about what a “proof” is, and what it will mean if the only viable way to solve such important questions going forward is with the help of computers.

Sighting the Beast

In principle, if you know the location and velocity of each particle in a fluid, the Euler equations should be able to predict how the fluid will evolve for all time. But mathematicians want to know if that’s actually the case. Perhaps in some situations, the equations will proceed as expected, producing precise values for the state of the fluid at any given moment, only for one of those values to suddenly skyrocket to infinity. At that point, the Euler equations are said to give rise to a “singularity” — or, more dramatically, to “blow up.”

Once they hit that singularity, the equations will no longer be able to compute the fluid’s flow. But “as of a few years ago, what people were able to do fell very, very far short of [proving blowup],” said Charlie Fefferman, a mathematician at Princeton University.

It gets even more complicated if you’re trying to model a fluid that has viscosity (as almost all real-world fluids do). A million-dollar Millennium Prize from the Clay Mathematics Institute awaits anyone who can prove whether similar failures occur in the Navier-Stokes equations, a generalization of the Euler equations that accounts for viscosity.

In 2013, Thomas Hou, a mathematician at the California Institute of Technology, and Guo Luo, now at the Hang Seng University of Hong Kong, proposed a scenario in which the Euler equations would lead to a singularity. They developed a computer simulation of a fluid in a cylinder whose top half swirled clockwise while its bottom half swirled counterclockwise. As they ran the simulation, more complicated currents started to move up and down. That, in turn, led to strange behavior along the boundary of the cylinder where opposing flows met. The fluid’s vorticity — a measure of rotation — grew so fast that it seemed poised to blow up.

Hou and Luo’s work was suggestive, but not a true proof. That’s because it’s impossible for a computer to calculate infinite values. It can get very close to seeing a singularity, but it can’t actually reach it — meaning that the solution might be very accurate, but it’s still an approximation. Without the backing of a mathematical proof, the value of the vorticity might only seem to be increasing to infinity because of some artifact of the simulation. The solutions might instead grow to enormous numbers before again subsiding.

Such reversals had happened before: A simulation would indicate that a value in the equations blew up, only for more sophisticated computational methods to show otherwise. “These problems are so delicate that the road is littered with the wreckage of previous simulations,” Fefferman said. In fact, that’s how Hou got his start in this area: Several of his earlier results disproved the formation of hypothetical singularities.

Still, when he and Luo published their solution, most mathematicians thought it was very likely a true singularity. “It was very meticulous, very precise,” said Vladimir Sverak, a mathematician at the University of Minnesota. “They really went to great lengths to establish that this is a real scenario.” Subsequent work by Elgindi, Sverak and others only strengthened that conviction.

But a proof was elusive. “You’ve sighted the beast,” Fefferman said. “Then you try to capture it.” That meant showing that the approximate solution that Hou and Luo so carefully simulated is, in a specific mathematical sense, very, very close to an exact solution of the equations.

Now, nine years after that first sighting, Hou and his former graduate student Jiajie Chen have finally succeeded in proving the existence of that nearby singularity.

The Move to Self-Similar Land

Hou, later joined by Chen, took advantage of the fact that, upon closer analysis, the approximate solution from 2013 seemed to have a special structure. As the equations evolved through time, the solution displayed what’s called a self-similar pattern: Its shape later on looked a lot like its earlier shape, only re-scaled in a specific way.

As a result, the mathematicians didn’t need to try to look at the singularity itself. Instead, they could study it indirectly by focusing on an earlier point in time. By zooming in on that part of the solution at the right rate — determined based on the solution’s self-similar structure — they could model what would happen later on, including at the singularity itself.

It took a few years for them to find a self-similar analogue to the 2013 blowup scenario. (Earlier this year, another team of mathematicians, which included Buckmaster, used different methods to find a similar approximate solution. They are currently using that solution to develop an independent proof of singularity formation.)

With an approximate self-similar solution in hand, Hou and Chen needed to show that an exact solution exists nearby. Mathematically, this is equivalent to proving that their approximate self-similar solution is stable — that even if you were to slightly perturb it and then evolve the equations starting at those perturbed values, there’d be no way to escape a small neighborhood around the approximate solution. “It’s like a black hole,” Hou said. “If you start with a profile close by, you’ll be sucked in.”

But having a general strategy was just one step toward the solution. “Fussy details matter,” Fefferman said. As Hou and Chen spent the next several years working out those details, they found that they had to rely on computers once again — but this time in an entirely new way.

A Hybrid Approach

Among their first challenges was figuring out the exact statement they had to prove. They wanted to show that if they took any set of values close to their approximate solution and plugged it into the equations, the output wouldn’t be able to stray far. But what does it mean for an input to be “close” to the approximate solution? They had to specify this in a mathematical statement — but there are many ways to define the notion of distance in this context. For their proof to work, they needed to choose the correct one.

“It has to measure different physical effects,” said Rafael de la Llave, a mathematician at the Georgia Institute of Technology. “So it needs to be chosen using a deep understanding of the problem.”

Once they had the right way to describe “closeness,” Hou and Chen had to prove the statement, which boiled down to a complicated inequality involving terms from both the re-scaled equations and the approximate solution. The mathematicians had to make sure that the values of all those terms balanced out to something very small: If one value ended up being large, other values had to be negative or kept in check.

“If you make something a little too big or a little too small, the whole thing breaks down,” said Javier Gómez-Serrano, a mathematician at Brown University. “So it’s very, very careful, delicate work.”

“It’s a really fierce fight,” Elgindi added.

To get the tight bounds they needed on all these different terms, Hou and Chen broke the inequality into two major parts. They could take care of the first part by hand, with techniques including one that dates back to the 18th century, when the French mathematician Gaspard Monge sought an optimal way of transporting soil to build fortifications for Napoleon’s army. “Stuff like this has been done before, but I found it striking that [Hou and Chen] used it for this,” Fefferman said.

That left the second part of the inequality. Tackling it would require computer assistance. For starters, there were so many calculations that needed to be done, and so much precision required, that “the amount of work you’d have to do with pencil and paper would be staggering,” de la Llave said. To get various terms to balance out, the mathematicians had to perform a series of optimization problems that are relatively easy for computers but exceedingly time-consuming for humans. Some of the values also depended on quantities from the approximate solution; since that was calculated using a computer, it was more straightforward to also use a computer to perform these additional computations.

“If you try to manually do some of these estimates, you’re probably going to overestimate at some point, and then you lose,” said Gómez-Serrano. “The numbers are so tiny and tight … and the margin is incredibly thin.”

But because computers can’t manipulate an infinite number of digits, tiny errors inevitably occur. Hou and Chen had to carefully track those errors, to make sure they didn’t interfere with the rest of the balancing act.

Ultimately, they were able to find bounds for all the terms, completing the proof: The equations had indeed produced a singularity.

Proof by Computer

It remains open whether more complicated equations — the Euler equations without the presence of a cylindrical boundary and the Navier-Stokes equations — can develop a singularity. “But [this work] at least gives me hope,” Hou said. “I see a path forward, a way to maybe even eventually resolve the full Millennium problem.”

Meanwhile, Buckmaster and Gómez-Serrano are working on a computer-assisted proof of their own — one they hope will be more general, and therefore capable of tackling not just the problem that Hou and Chen solved, but also scores of others.

These efforts mark a growing trend in the field of fluid dynamics: the use of computers to solve important problems.

“In a number of different areas of mathematics, it’s occurring more and more frequently,” said Susan Friedlander, a mathematician at the University of Southern California.

But in fluid mechanics, computer-assisted proofs are still a relatively new technique. In fact, when it comes to statements about singularity formation, Hou and Chen’s proof is the first of its kind: Previous computer-assisted proofs were only able to tackle toy problems in the area.

Such proofs aren’t so much controversial as “a matter of taste,” said Peter Constantin of Princeton University. Mathematicians generally agree that a proof has to convince other mathematicians that some line of reasoning is correct. But, many argue, it should also improve their understanding of why a particular statement is true, rather than simply provide validation that it’s correct. “Do we learn anything fundamentally new, or do we just know the answer to the question?” Elgindi said. “If you view mathematics as an art, then this is not so aesthetically pleasing.”

“A computer can help. It’s wonderful. It gives me insight. But it doesn’t give me a full understanding,” Constantin added. “Understanding comes from us.”

For his part, Elgindi still hopes to work out an alternative proof of blowup entirely by hand. “I’m overall happy this exists,” he said of Hou and Chen’s work. “But I take it as more of a motivation to try to do it in a less computer-dependent way.”

Other mathematicians view computers as a vital new tool that will make it possible to attack previously intractable problems. “Now the work is no longer just paper and pencil,” Chen said. “You have the option of using something more powerful.”

According to him and others (including Elgindi, despite his personal preference for writing proofs by hand), there’s a good possibility that the only way to solve big problems in fluid dynamics — that is, problems that involve increasingly complicated equations — might be to rely heavily on computer assistance. “It looks to me as if trying to do this without making heavy use of computer-assisted proofs is like tying one or possibly two hands behind your back,” Fefferman said.

If that does end up being the case and “you don’t have any choice,” Elgindi said, “then people … such as myself, who would say that this is suboptimal, should be quiet.” That would also mean that more mathematicians would need to start learning the skills needed to write computer-assisted proofs — something that Hou and Chen’s work will hopefully inspire. “I think there were a lot of people who were simply waiting for someone to solve such a problem before investing any of their own time into this approach,” Buckmaster said.

That said, when it comes to debates about the extent to which mathematicians should rely on computers, “it’s not that you need to pick a side,” Gómez-Serrano said. “[Hou and Chen’s] proof wouldn’t work without the analysis, and the proof wouldn’t work without the computer assistance. … I think the value is that people can speak the two languages.”

With that, de la Llave said, “there’s a new game in town.”