Introduktion
I århundreder har matematikere søgt at forstå og modellere væskers bevægelse. Ligningerne, der beskriver, hvordan krusninger folder overfladen af en dam, har også hjulpet forskere med at forudsige vejret, designe bedre fly og karakterisere, hvordan blodet strømmer gennem kredsløbssystemet. Disse ligninger er vildledende enkle, når de er skrevet i det rigtige matematiske sprog. Men deres løsninger er så komplekse, at det kan være uoverkommeligt svært at give mening med selv grundlæggende spørgsmål om dem.
Måske den ældste og mest fremtrædende af disse ligninger, formuleret af Leonhard Euler for mere end 250 år siden, beskriver strømmen af en ideel, inkompressibel væske: en væske uden viskositet eller indre friktion, som ikke kan tvinges ind i et mindre volumen. "Næsten alle ikke-lineære væskeligninger er på en måde afledt af Euler-ligningerne," sagde Tarek Elgindi, matematiker ved Duke University. "De er de første, kan man sige."
Alligevel er meget ukendt om Euler-ligningerne - herunder om de altid er en nøjagtig model for ideel væskestrøm. Et af de centrale problemer i væskedynamik er at finde ud af, om ligningerne nogensinde fejler, og udsender meningsløse værdier, der gør dem ude af stand til at forudsige en væskes fremtidige tilstande.
Matematikere har længe haft mistanke om, at der eksisterer begyndelsesbetingelser, der får ligningerne til at bryde sammen. Men de har ikke været i stand til at bevise det.
In et fortryk udgivet online i sidste måned, har et par matematikere vist, at en bestemt version af Euler-ligningerne faktisk nogle gange fejler. Beviset markerer et stort gennembrud - og selvom det ikke helt løser problemet for den mere generelle version af ligningerne, giver det håb om, at en sådan løsning endelig er inden for rækkevidde. "Det er et fantastisk resultat," sagde Tristan Buckmaster, en matematiker ved University of Maryland, som ikke var involveret i arbejdet. "Der er ingen resultater af denne art i litteraturen."
Der er kun en fangst.
Det 177 sider lange bevis - resultatet af et årti langt forskningsprogram - gør betydelig brug af computere. Dette gør det uden tvivl vanskeligt for andre matematikere at verificere det. (Faktisk er de stadig i gang med at gøre det, selvom mange eksperter mener, at det nye arbejde vil vise sig at være korrekt.) Det tvinger dem også til at regne med filosofiske spørgsmål om, hvad et "bevis" er, og hvad det vil mener, hvis den eneste levedygtige måde at løse så vigtige spørgsmål fremadrettet er ved hjælp af computere.
At se Udyret
I princippet, hvis du kender placeringen og hastigheden af hver partikel i en væske, burde Euler-ligningerne være i stand til at forudsige, hvordan væsken vil udvikle sig for altid. Men matematikere vil gerne vide, om det faktisk er tilfældet. Måske i nogle situationer vil ligningerne fortsætte som forventet og producere præcise værdier for væskens tilstand på ethvert givet tidspunkt, kun for en af disse værdier pludselig at skyde i vejret til det uendelige. På det tidspunkt siges Euler-ligningerne at give anledning til en "singularitet" - eller mere dramatisk at "sprænge i luften".
Når først de rammer den singularitet, vil ligningerne ikke længere være i stand til at beregne væskens flow. Men "som for et par år siden, var det, folk var i stand til at gøre, meget, meget langt fra [at bevise blowup]," sagde Charlie Fefferman, matematiker ved Princeton University.
Det bliver endnu mere kompliceret, hvis du prøver at modellere en væske, der har viskositet (som næsten alle væsker i den virkelige verden gør). En million-dollar Millennium-pris fra Clay Mathematics Institute venter på enhver, der kan bevise, om lignende fejl forekommer i Navier-Stokes-ligningerne, en generalisering af Euler-ligningerne, der tegner sig for viskositet.
I 2013, blev Thomas Hou, matematiker ved California Institute of Technology, og Guo Luo, nu ved Hang Seng University of Hong Kong, foreslog et scenarie, hvor Euler-ligningerne ville føre til en singularitet. De udviklede en computersimulering af en væske i en cylinder, hvis øverste halvdel hvirvlede med uret, mens dens nederste halvdel hvirvlede mod uret. Da de kørte simuleringen, begyndte mere komplicerede strømme at bevæge sig op og ned. Det førte til gengæld til mærkelig adfærd langs cylinderens grænse, hvor modsatrettede strømme mødtes. Væskens hvirvelstrøm - et mål for rotation - voksede så hurtigt, at det så ud til at blæse op.
Hou og Luos arbejde var tankevækkende, men ikke et sandt bevis. Det er fordi det er umuligt for en computer at beregne uendelige værdier. Det kan komme meget tæt på at se en singularitet, men det kan faktisk ikke nå det - hvilket betyder, at løsningen kan være meget nøjagtig, men det er stadig en tilnærmelse. Uden støtte fra et matematisk bevis kan værdien af hvirvlen kun synes at være stigende til det uendelige på grund af en eller anden artefakt af simuleringen. Løsningerne kan i stedet vokse til enorme tal, før de igen aftager.
Sådanne vendinger var sket før: En simulering ville indikere, at en værdi i ligningerne eksploderede, kun for mere sofistikerede beregningsmetoder at vise andet. "Disse problemer er så delikate, at vejen er fyldt med vragdele fra tidligere simuleringer," sagde Fefferman. Faktisk var det sådan, Hou fik sin start på dette område: Flere af hans tidligere resultater modbeviste dannelsen af hypotetiske singulariteter.
Alligevel, da han og Luo offentliggjorde deres løsning, troede de fleste matematikere, at det meget sandsynligt var en ægte singularitet. "Det var meget omhyggeligt, meget præcist," sagde Vladimir Sverak, matematiker ved University of Minnesota. "De gik virkelig meget langt for at fastslå, at dette er et rigtigt scenarie." Efterfølgende arbejde af Elgindi, Sverak m.fl kun styrket den overbevisning.
Men et bevis var undvigende. "Du har set udyret," sagde Fefferman. "Så prøver du at fange det." Det betød at vise, at den omtrentlige løsning, som Hou og Luo så omhyggeligt simulerede, i en specifik matematisk forstand er meget, meget tæt på en nøjagtig løsning af ligningerne.
Nu, ni år efter den første observation, Hou og hans tidligere kandidatstuderende Jiajie Chen er det endelig lykkedes at bevise eksistensen af den nærliggende singularitet.
Flytningen til selv-lignende land
Hou, senere sammen med Chen, udnyttede det faktum, at den omtrentlige løsning fra 2013 ved en nærmere analyse så ud til at have en særlig struktur. Efterhånden som ligningerne udviklede sig gennem tiden, viste løsningen det, der kaldes et selv-lignende mønster: Dens form lignede senere meget dens tidligere form, kun omskaleret på en bestemt måde.
Som et resultat behøvede matematikerne ikke at prøve at se på selve singulariteten. I stedet kunne de studere det indirekte ved at fokusere på et tidligere tidspunkt. Ved at zoome ind på den del af løsningen med den rigtige hastighed - bestemt ud fra løsningens selv-lignende struktur - kunne de modellere, hvad der ville ske senere, inklusive ved selve singulariteten.
Det tog et par år for dem at finde en selvlignende analog til 2013-blowup-scenariet. (Tidligere i år brugte et andet team af matematikere, som inkluderede Buckmaster, forskellige metoder til at finde en lignende omtrentlig løsning. De bruger i øjeblikket den løsning til at udvikle et uafhængigt bevis på singularitetsdannelse.)
Med en omtrentlig selvlignende løsning i hånden, var Hou og Chen nødt til at vise, at der findes en nøjagtig løsning i nærheden. Matematisk svarer dette til at bevise, at deres omtrentlige selv-lignende løsning er stabil - at selv hvis du skulle forstyrre den en smule og derefter udvikle ligningerne startende ved de forstyrrede værdier, ville der ikke være nogen måde at undslippe et lille kvarter omkring omtrentlig løsning. "Det er som et sort hul," sagde Hou. "Hvis du starter med en profil tæt på, bliver du suget ind."
Men at have en generel strategi var kun et skridt mod løsningen. "Kræsne detaljer betyder noget," sagde Fefferman. Mens Hou og Chen brugte de næste mange år på at udarbejde disse detaljer, fandt de ud af, at de var nødt til at stole på computere igen - men denne gang på en helt ny måde.
En hybrid tilgang
Blandt deres første udfordringer var at finde ud af det præcise udsagn, de skulle bevise. De ønskede at vise, at hvis de tog et sæt værdier tæt på deres omtrentlige løsning og tilsluttede det i ligningerne, ville outputtet ikke være i stand til at afvige langt. Men hvad betyder det, at et input er "tæt" på den omtrentlige løsning? De var nødt til at specificere dette i en matematisk erklæring - men der er mange måder at definere begrebet afstand på i denne sammenhæng. For at deres bevis skulle virke, var de nødt til at vælge den rigtige.
"Det skal måle forskellige fysiske effekter," sagde Rafael de la Llave, en matematiker ved Georgia Institute of Technology. "Så det skal vælges ud fra en dyb forståelse af problemet."
Da de først havde den rigtige måde at beskrive "nærhed på", skulle Hou og Chen bevise udsagnet, som kogte ned til en kompliceret ulighed, der involverede termer fra både de omskalerede ligninger og den omtrentlige løsning. Matematikerne skulle sørge for, at værdierne af alle disse udtryk balancerede til noget meget lille: Hvis en værdi endte med at være stor, skulle andre værdier være negative eller holdes i skak.
"Hvis du laver noget lidt for stort eller lidt for lille, går det hele i stykker," sagde Javier Gómez-Serrano, matematiker ved Brown University. "Så det er meget, meget omhyggeligt, delikat arbejde."
"Det er en virkelig hård kamp," tilføjede Elgindi.
For at få de stramme grænser, de havde brug for på alle disse forskellige vilkår, brød Hou og Chen uligheden op i to store dele. De kunne tage sig af den første del i hånden, med teknikker, herunder en, der går tilbage til det 18. århundrede, hvor den franske matematiker Gaspard Monge søgte en optimal måde at transportere jord på for at bygge befæstninger til Napoleons hær. "Ting som dette er blevet gjort før, men jeg fandt det slående, at [Hou og Chen] brugte det til dette," sagde Fefferman.
Det efterlod den anden del af uligheden. At tackle det ville kræve computerhjælp. Til at begynde med var der så mange beregninger, der skulle udføres, og der krævedes så meget præcision, at "mængden af arbejde, du skulle gøre med blyant og papir, ville være svimlende," sagde de la Llave. For at få forskellige udtryk til at balancere, måtte matematikerne udføre en række optimeringsproblemer, der er relativt nemme for computere, men ekstremt tidskrævende for mennesker. Nogle af værdierne afhang også af mængder fra den omtrentlige løsning; da det blev beregnet ved hjælp af en computer, var det mere ligetil også at bruge en computer til at udføre disse ekstra beregninger.
"Hvis du prøver at lave nogle af disse estimater manuelt, vil du sandsynligvis overvurdere på et tidspunkt, og så taber du," sagde Gómez-Serrano. "Tallene er så små og stramme ... og margenen er utrolig tynd."
Men fordi computere ikke kan manipulere et uendeligt antal cifre, opstår der uundgåeligt små fejl. Hou og Chen måtte omhyggeligt spore disse fejl for at sikre, at de ikke forstyrrede resten af balancegangen.
I sidste ende var de i stand til at finde grænser for alle vilkårene og fuldende beviset: Ligningerne havde faktisk frembragt en singularitet.
Bevis ved computer
Det er stadig åbent, om mere komplicerede ligninger - Euler-ligningerne uden tilstedeværelsen af en cylindrisk grænse og Navier-Stokes-ligningerne - kan udvikle en singularitet. "Men [dette arbejde] giver mig i det mindste håb," sagde Hou. "Jeg ser en vej frem, en måde at måske endda i sidste ende løse det fulde Millennium-problem."
I mellemtiden arbejder Buckmaster og Gómez-Serrano på deres eget computerstøttede bevis - et, som de håber vil være mere generelt, og derfor i stand til at tackle ikke bare det problem, som Hou og Chen løste, men også snesevis af andre.
Disse bestræbelser markerer en voksende tendens inden for fluiddynamik: brugen af computere til at løse vigtige problemer.
"På en række forskellige områder af matematikken forekommer det oftere og oftere," sagde Susan Friedlander, en matematiker ved University of Southern California.
Men i væskemekanik er computerstøttede beviser stadig en relativt ny teknik. Faktisk, når det kommer til udsagn om singularitetsdannelse, er Hou og Chens bevis det første af sin slags: Tidligere computerstøttede beviser var kun i stand til at tackle legetøjsproblemer i området.
Sådanne beviser er ikke så meget kontroversielle som "et spørgsmål om smag," sagde Peter Constantin fra Princeton University. Matematikere er generelt enige om, at et bevis skal overbevise andre matematikere om, at en eller anden ræsonnement er korrekt. Men, hævder mange, det burde også forbedre deres forståelse af, hvorfor et bestemt udsagn er sandt, snarere end blot at bekræfte, at det er korrekt. "Lærer vi noget grundlæggende nyt, eller kender vi bare svaret på spørgsmålet?" sagde Elgindi. "Hvis du ser matematik som en kunst, så er det ikke så æstetisk tiltalende."
"En computer kan hjælpe. Det er vidunderligt. Det giver mig indsigt. Men det giver mig ikke fuld forståelse,” tilføjede Constantin. "Forståelse kommer fra os."
På sin side håber Elgindi stadig på at udarbejde et alternativt bevis for blowup helt i hånden. "Jeg er overordnet glad for, at dette eksisterer," sagde han om Hou og Chens arbejde. "Men jeg ser det mere som en motivation at prøve at gøre det på en mindre computerafhængig måde."
Andre matematikere ser computere som et vigtigt nyt værktøj, der vil gøre det muligt at angribe tidligere vanskelige problemer. "Nu er arbejdet ikke længere kun papir og blyant," sagde Chen. "Du har mulighed for at bruge noget mere kraftfuldt."
Ifølge ham og andre (inklusive Elgindi, på trods af hans personlige præference for at skrive korrektur i hånden), er der en god mulighed for, at den eneste måde at løse store problemer i væskedynamik - det vil sige problemer, der involverer stadig mere komplicerede ligninger - kan være at stole på meget på computerhjælp. "Det ser for mig ud, som om at prøve at gøre dette uden at gøre stor brug af computerstøttede beviser er som at binde en eller muligvis to hænder bag ryggen," sagde Fefferman.
Hvis det ender med at være tilfældet, og "du ikke har noget valg," sagde Elgindi, "så burde folk ... såsom mig selv, der ville sige, at dette er suboptimalt, tie stille." Det ville også betyde, at flere matematikere skulle begynde at lære de nødvendige færdigheder til at skrive computerstøttede korrektur - noget som Hou og Chens arbejde forhåbentlig vil inspirere. "Jeg tror, der var mange mennesker, der simpelthen ventede på, at nogen skulle løse et sådant problem, før de investerede noget af deres egen tid i denne tilgang," sagde Buckmaster.
Når det er sagt, når det kommer til debatter om, i hvilket omfang matematikere bør stole på computere, "er det ikke, at du skal vælge en side," sagde Gómez-Serrano. "[Hou og Chens] bevis ville ikke fungere uden analysen, og beviset ville ikke fungere uden computerassistance. ... Jeg tror, værdien er, at folk kan tale de to sprog."
Med det sagde de la Llave, "der er et nyt spil i byen."
