Introduction
Pendant des siècles, les mathématiciens ont cherché à comprendre et à modéliser le mouvement des fluides. Les équations qui décrivent comment les ondulations plissent la surface d'un étang ont également aidé les chercheurs à prédire le temps, à concevoir de meilleurs avions et à caractériser la circulation du sang dans le système circulatoire. Ces équations sont d'une simplicité trompeuse lorsqu'elles sont écrites dans le bon langage mathématique. Cependant, leurs solutions sont si complexes qu'il peut être extrêmement difficile de donner un sens aux questions les plus élémentaires à leur sujet.
Peut-être la plus ancienne et la plus importante de ces équations, formulée par Leonhard Euler il y a plus de 250 ans, décrit l'écoulement d'un fluide idéal et incompressible : un fluide sans viscosité ni frottement interne, qui ne peut pas être forcé dans un volume plus petit. "Presque toutes les équations de fluides non linéaires sont en quelque sorte dérivées des équations d'Euler", a déclaré Tarek Elgindi, mathématicien à Duke University. "Ce sont les premiers, pourrait-on dire."
Pourtant, il reste beaucoup d'inconnues sur les équations d'Euler, y compris si elles sont toujours un modèle précis d'écoulement de fluide idéal. L'un des problèmes centraux de la dynamique des fluides est de déterminer si les équations échouent, produisant des valeurs absurdes qui les rendent incapables de prédire les états futurs d'un fluide.
Les mathématiciens soupçonnent depuis longtemps qu'il existe des conditions initiales qui provoquent la rupture des équations. Mais ils n'ont pas été en mesure de le prouver.
In une préimpression mis en ligne le mois dernier, un duo de mathématiciens a montré qu'une version particulière des équations d'Euler échoue effectivement parfois. La preuve marque une percée majeure - et bien qu'elle ne résolve pas complètement le problème pour la version plus générale des équations, elle laisse espérer qu'une telle solution est enfin à portée de main. "C'est un résultat incroyable", a déclaré Tristan Buckmaster, un mathématicien de l'Université du Maryland qui n'a pas participé aux travaux. "Il n'y a pas de résultats de ce genre dans la littérature."
Il n'y a qu'un hic.
La preuve de 177 pages - le résultat d'un programme de recherche d'une décennie - fait un usage important des ordinateurs. Cela rend sans doute difficile pour les autres mathématiciens de le vérifier. (En fait, ils sont toujours en train de le faire, bien que de nombreux experts pensent que le nouveau travail s'avérera correct.) Cela les oblige également à tenir compte des questions philosophiques sur ce qu'est une "preuve" et ce qu'elle signifie si la seule façon viable de résoudre des questions aussi importantes à l'avenir est à l'aide d'ordinateurs.
Apercevoir la bête
En principe, si vous connaissez l'emplacement et la vitesse de chaque particule dans un fluide, les équations d'Euler devraient pouvoir prédire comment le fluide évoluera pour toujours. Mais les mathématiciens veulent savoir si c'est réellement le cas. Peut-être que dans certaines situations, les équations se dérouleront comme prévu, produisant des valeurs précises pour l'état du fluide à un moment donné, seulement pour qu'une de ces valeurs monte soudainement en flèche à l'infini. À ce stade, on dit que les équations d'Euler donnent lieu à une "singularité" - ou, plus dramatiquement, à "exploser".
Une fois qu'elles auront atteint cette singularité, les équations ne pourront plus calculer le débit du fluide. Mais "il y a quelques années, ce que les gens étaient capables de faire était très, très loin de [proving blowup]", a déclaré Charlie Feffermann, mathématicien à l'université de Princeton.
Cela devient encore plus compliqué si vous essayez de modéliser un fluide qui a de la viscosité (comme le font presque tous les fluides du monde réel). Un prix du millénaire d'un million de dollars du Clay Mathematics Institute attend tous ceux qui peuvent prouver si des échecs similaires se produisent dans les équations de Navier-Stokes, une généralisation des équations d'Euler qui explique la viscosité.
En 2013, Thomas Hou, mathématicien au California Institute of Technology, et Guo Luo, maintenant à l'Université Hang Seng de Hong Kong, a proposé un scénario dans lequel les équations d'Euler conduiraient à une singularité. Ils ont développé une simulation informatique d'un fluide dans un cylindre dont la moitié supérieure tourbillonnait dans le sens des aiguilles d'une montre tandis que sa moitié inférieure tourbillonnait dans le sens inverse des aiguilles d'une montre. Au fur et à mesure qu'ils exécutaient la simulation, des courants plus compliqués ont commencé à monter et descendre. Cela, à son tour, a conduit à un comportement étrange le long de la limite du cylindre où des flux opposés se sont rencontrés. La vorticité du fluide - une mesure de rotation - a augmenté si rapidement qu'il semblait sur le point d'exploser.
Le travail de Hou et Luo était suggestif, mais pas une vraie preuve. C'est parce qu'il est impossible pour un ordinateur de calculer des valeurs infinies. Il peut être très proche de voir une singularité, mais il ne peut pas réellement l'atteindre - ce qui signifie que la solution peut être très précise, mais c'est toujours une approximation. Sans l'appui d'une preuve mathématique, la valeur de la vorticité pourrait ne sembler augmenter qu'à l'infini à cause d'un artefact de la simulation. Les solutions pourraient plutôt atteindre un nombre énorme avant de retomber.
De tels renversements s'étaient produits auparavant : une simulation indiquerait qu'une valeur dans les équations a explosé, seulement pour que des méthodes de calcul plus sophistiquées montrent le contraire. "Ces problèmes sont si délicats que la route est jonchée des décombres des simulations précédentes", a déclaré Fefferman. En fait, c'est ainsi que Hou a fait ses débuts dans ce domaine : plusieurs de ses résultats antérieurs ont réfuté la formation de singularités hypothétiques.
Pourtant, quand lui et Luo ont publié leur solution, la plupart des mathématiciens pensaient qu'il s'agissait très probablement d'une véritable singularité. "C'était très méticuleux, très précis", a déclaré Vladimir Svérak, mathématicien à l'Université du Minnesota. "Ils se sont vraiment donné beaucoup de mal pour établir qu'il s'agit d'un scénario réel." Travaux ultérieurs d'Elgindi, Sverak et d'autres n'a fait que renforcer cette conviction.
Mais une preuve était insaisissable. "Vous avez aperçu la bête", a déclaré Fefferman. "Ensuite, vous essayez de le capturer." Cela signifiait montrer que la solution approximative que Hou et Luo ont si soigneusement simulée est, dans un sens mathématique spécifique, très, très proche d'une solution exacte des équations.
Maintenant, neuf ans après cette première observation, Hou et son ancien étudiant diplômé Jiajie Chen ont finalement réussi à prouver l'existence de cette singularité proche.
Le déménagement vers des terres auto-similaires
Hou, rejoint plus tard par Chen, a profité du fait que, après une analyse plus approfondie, la solution approximative de 2013 semblait avoir une structure particulière. Au fur et à mesure que les équations évoluaient dans le temps, la solution affichait ce qu'on appelle un motif auto-similaire : sa forme ressemblait beaucoup plus tard à sa forme précédente, mais redimensionnée d'une manière spécifique.
En conséquence, les mathématiciens n'ont pas eu besoin d'essayer de regarder la singularité elle-même. Au lieu de cela, ils pourraient l'étudier indirectement en se concentrant sur un point antérieur dans le temps. En zoomant sur cette partie de la solution au bon taux - déterminé en fonction de la structure auto-similaire de la solution - ils pourraient modéliser ce qui se passerait plus tard, y compris au niveau de la singularité elle-même.
Il leur a fallu quelques années pour trouver un analogue auto-similaire au scénario d'explosion de 2013. (Plus tôt cette année, une autre équipe de mathématiciens, qui comprenait Buckmaster, a utilisé différentes méthodes pour trouver une solution approchée similaire. Ils utilisent actuellement cette solution pour développer une preuve indépendante de la formation de singularités.)
Avec une solution auto-similaire approchée en main, Hou et Chen devaient montrer qu'une solution exacte existe à proximité. Mathématiquement, cela équivaut à prouver que leur solution auto-similaire approximative est stable - que même si vous deviez la perturber légèrement et ensuite faire évoluer les équations à partir de ces valeurs perturbées, il n'y aurait aucun moyen d'échapper à un petit voisinage autour de la solution approximative. "C'est comme un trou noir", a déclaré Hou. "Si vous commencez avec un profil à proximité, vous serez aspiré."
Mais avoir une stratégie générale n'était qu'un pas vers la solution. "Les détails difficiles comptent", a déclaré Fefferman. Alors que Hou et Chen passaient les années suivantes à travailler sur ces détails, ils ont constaté qu'ils devaient à nouveau compter sur les ordinateurs - mais cette fois d'une manière entièrement nouvelle.
Une approche hybride
L'un de leurs premiers défis consistait à déterminer la déclaration exacte qu'ils devaient prouver. Ils voulaient montrer que s'ils prenaient n'importe quel ensemble de valeurs proches de leur solution approximative et le branchaient dans les équations, la sortie ne pourrait pas s'égarer loin. Mais qu'est-ce que cela signifie pour une entrée d'être « proche » de la solution approximative ? Ils devaient le préciser dans un énoncé mathématique — mais il existe de nombreuses façons de définir la notion de distance dans ce contexte. Pour que leur preuve fonctionne, ils devaient choisir la bonne.
"Il doit mesurer différents effets physiques", a déclaré Raphaël de la Llave, mathématicien au Georgia Institute of Technology. "Il doit donc être choisi en utilisant une compréhension approfondie du problème."
Une fois qu'ils ont trouvé la bonne façon de décrire la «proximité», Hou et Chen ont dû prouver l'affirmation, qui se résumait à une inégalité compliquée impliquant à la fois des termes des équations rééchelonnées et de la solution approximative. Les mathématiciens devaient s'assurer que les valeurs de tous ces termes s'équilibraient à quelque chose de très petit : si une valeur finissait par être grande, les autres valeurs devaient être négatives ou contrôlées.
"Si vous faites quelque chose d'un peu trop grand ou d'un peu trop petit, tout s'effondre", a déclaré Javier Gómez-Serrano, mathématicien à l'Université Brown. "C'est donc un travail très, très minutieux et délicat."
"C'est un combat vraiment féroce", a ajouté Elgindi.
Pour obtenir les limites étroites dont ils avaient besoin sur tous ces termes différents, Hou et Chen ont divisé l'inégalité en deux parties principales. Ils pouvaient s'occuper de la première partie à la main, avec des techniques dont une qui remonte au XVIIIe siècle, lorsque le mathématicien français Gaspard Monge chercha un moyen optimal de transporter de la terre pour construire des fortifications pour l'armée de Napoléon. "Des choses comme celle-ci ont déjà été faites, mais j'ai trouvé frappant que [Hou et Chen] l'aient utilisé pour cela", a déclaré Fefferman.
Restait la deuxième partie de l'inégalité. Pour y remédier, il faudrait une assistance informatique. Pour commencer, il y avait tellement de calculs à faire et tellement de précision requise que "la quantité de travail que vous auriez à faire avec un crayon et du papier serait stupéfiante", a déclaré de la Llave. Pour équilibrer les différents termes, les mathématiciens ont dû résoudre une série de problèmes d'optimisation qui sont relativement simples pour les ordinateurs mais extrêmement chronophages pour les humains. Certaines des valeurs dépendaient également des quantités de la solution approximative; puisque cela a été calculé à l'aide d'un ordinateur, il était plus simple d'utiliser également un ordinateur pour effectuer ces calculs supplémentaires.
"Si vous essayez de faire manuellement certaines de ces estimations, vous allez probablement surestimer à un moment donné, puis vous perdrez", a déclaré Gómez-Serrano. "Les chiffres sont si minuscules et serrés … et la marge est incroyablement mince."
Mais parce que les ordinateurs ne peuvent pas manipuler un nombre infini de chiffres, de petites erreurs se produisent inévitablement. Hou et Chen ont dû suivre attentivement ces erreurs, pour s'assurer qu'elles n'interféraient pas avec le reste de l'exercice d'équilibre.
En fin de compte, ils ont pu trouver des bornes pour tous les termes, complétant la preuve : les équations avaient en effet produit une singularité.
Preuve par ordinateur
Il reste ouvert si des équations plus compliquées - les équations d'Euler sans la présence d'une frontière cylindrique et les équations de Navier-Stokes - peuvent développer une singularité. "Mais [ce travail] me donne au moins de l'espoir", a déclaré Hou. "Je vois une voie à suivre, un moyen peut-être même éventuellement de résoudre le problème du millénaire dans son ensemble."
Pendant ce temps, Buckmaster et Gómez-Serrano travaillent sur leur propre preuve assistée par ordinateur – une preuve qu'ils espèrent être plus générale, et donc capable de s'attaquer non seulement au problème que Hou et Chen ont résolu, mais aussi à des dizaines d'autres.
Ces efforts marquent une tendance croissante dans le domaine de la dynamique des fluides : l'utilisation des ordinateurs pour résoudre des problèmes importants.
"Dans un certain nombre de domaines différents des mathématiques, cela se produit de plus en plus fréquemment", a déclaré Susan Friedländer, mathématicien à l'Université de Californie du Sud.
Mais en mécanique des fluides, les preuves assistées par ordinateur sont encore une technique relativement nouvelle. En fait, en ce qui concerne les affirmations sur la formation des singularités, la preuve de Hou et Chen est la première du genre : les preuves assistées par ordinateur précédentes ne pouvaient résoudre que les problèmes de jouet dans la région.
De telles preuves ne sont pas tant controversées qu'"une question de goût", a déclaré Pierre Constantin de l'Université de Princeton. Les mathématiciens conviennent généralement qu'une preuve doit convaincre les autres mathématiciens qu'un raisonnement est correct. Mais, selon beaucoup, cela devrait également améliorer leur compréhension de la raison pour laquelle une affirmation particulière est vraie, plutôt que de simplement fournir une validation qu'elle est correcte. "Apprenons-nous quelque chose de fondamentalement nouveau, ou connaissons-nous simplement la réponse à la question?" dit Elgindi. "Si vous considérez les mathématiques comme un art, alors ce n'est pas si esthétique."
« Un ordinateur peut aider. C'est merveilleux. Cela me donne un aperçu. Mais cela ne me donne pas une compréhension complète », a ajouté Constantin. "La compréhension vient de nous."
De son côté, Elgindi espère toujours élaborer une preuve alternative d'explosion entièrement à la main. "Je suis globalement heureux que cela existe", a-t-il déclaré à propos du travail de Hou et Chen. "Mais je le considère plus comme une motivation pour essayer de le faire d'une manière moins dépendante de l'ordinateur."
D'autres mathématiciens considèrent les ordinateurs comme un nouvel outil vital qui permettra de s'attaquer à des problèmes auparavant insolubles. "Maintenant, le travail n'est plus seulement du papier et un crayon", a déclaré Chen. "Vous avez la possibilité d'utiliser quelque chose de plus puissant."
Selon lui et d'autres (y compris Elgindi, malgré sa préférence personnelle pour l'écriture de preuves à la main), il y a une bonne possibilité que la seule façon de résoudre de gros problèmes de dynamique des fluides - c'est-à-dire des problèmes qui impliquent des équations de plus en plus compliquées - soit de s'appuyer fortement sur l'assistance informatique. "Il me semble qu'essayer de faire cela sans faire un usage intensif de preuves assistées par ordinateur revient à attacher une ou peut-être deux mains derrière le dos", a déclaré Fefferman.
Si cela finit par être le cas et que "vous n'avez pas le choix", a déclaré Elgindi, "alors les gens... comme moi, qui diraient que c'est sous-optimal, devraient se taire." Cela signifierait également que davantage de mathématiciens devraient commencer à acquérir les compétences nécessaires pour écrire des preuves assistées par ordinateur – quelque chose que le travail de Hou et Chen inspirera, espérons-le. "Je pense qu'il y avait beaucoup de gens qui attendaient simplement que quelqu'un résolve un tel problème avant d'investir de leur temps dans cette approche", a déclaré Buckmaster.
Cela dit, lorsqu'il s'agit de débats sur la mesure dans laquelle les mathématiciens devraient s'appuyer sur les ordinateurs, "ce n'est pas que vous devez choisir un camp", a déclaré Gómez-Serrano. « La preuve [de Hou et Chen] ne fonctionnerait pas sans l'analyse, et la preuve ne fonctionnerait pas sans l'assistance informatique. … Je pense que la valeur est que les gens peuvent parler les deux langues.
Avec cela, de la Llave a dit, "il y a un nouveau jeu en ville."
