Komputerowy dowód „wysadza w powietrze” wielowiekowe równania płynów PlatoBlockchain Data Intelligence. Wyszukiwanie pionowe. AI.

Komputerowy dowód „wysadza w powietrze” wielowiekowe równania płynów

Wprowadzenie

Od wieków matematycy starali się zrozumieć i modelować ruch płynów. Równania, które opisują, w jaki sposób zmarszczki marszczą powierzchnię stawu, pomogły również naukowcom przewidywać pogodę, projektować lepsze samoloty i charakteryzować przepływ krwi przez układ krążenia. Te równania są zwodniczo proste, gdy są zapisane we właściwym języku matematycznym. Jednak ich rozwiązania są tak złożone, że zrozumienie nawet podstawowych pytań na ich temat może być niezwykle trudne.

Być może najstarsze i najbardziej znane z tych równań, sformułowane przez Leonharda Eulera ponad 250 lat temu, opisują przepływ idealnego, nieściśliwego płynu: płynu bez lepkości lub tarcia wewnętrznego, którego nie można zmusić do zmniejszenia objętości. „Prawie wszystkie nieliniowe równania płynów wywodzą się z równań Eulera” – powiedział Tarka Elgindiego, matematyk z Duke University. „Można powiedzieć, że są pierwsi”.

Jednak wiele pozostaje nieznanych na temat równań Eulera - w tym, czy są one zawsze dokładnym modelem idealnego przepływu płynu. Jednym z głównych problemów w dynamice płynów jest ustalenie, czy równania kiedykolwiek zawodzą, generując bezsensowne wartości, które uniemożliwiają przewidywanie przyszłych stanów płynu.

Matematycy od dawna podejrzewali, że istnieją warunki początkowe, które powodują załamanie równań. Ale nie udało im się tego udowodnić.

In wydruk wstępny opublikowana w Internecie w zeszłym miesiącu, para matematyków wykazała, że ​​określona wersja równań Eulera rzeczywiście czasami zawodzi. Dowód stanowi ważny przełom — i chociaż nie rozwiązuje całkowicie problemu dla bardziej ogólnej wersji równań, daje nadzieję, że takie rozwiązanie jest w końcu w zasięgu ręki. „To niesamowity wynik” — powiedział Tristana Buckmastera, matematyk z University of Maryland, który nie był zaangażowany w pracę. „W literaturze nie ma wyników tego rodzaju”.

Jest tylko jeden haczyk.

177-stronicowy dowód — wynik dziesięcioletniego programu badawczego — w znacznym stopniu wykorzystuje komputery. To prawdopodobnie utrudnia innym matematykom zweryfikowanie tego. (Właściwie są jeszcze w trakcie tego procesu, choć wielu ekspertów uważa, że ​​nowa praca okaże się poprawna.) Zmusza ich także do rozliczenia się z filozoficznymi pytaniami o to, czym jest „dowód” i do czego będzie służył. oznaczać, że jedynym realnym sposobem rozwiązania tak ważnych kwestii w przyszłości jest pomoc komputerów.

Widzenie Bestii

W zasadzie, jeśli znasz położenie i prędkość każdej cząstki w płynie, równania Eulera powinny być w stanie przewidzieć, jak płyn będzie ewoluował przez cały czas. Ale matematycy chcą wiedzieć, czy tak jest w rzeczywistości. Być może w niektórych sytuacjach równania będą przebiegać zgodnie z oczekiwaniami, dając dokładne wartości stanu płynu w danym momencie, tylko po to, by jedna z tych wartości nagle gwałtownie wzrosła do nieskończoności. W tym momencie mówi się, że równania Eulera powodują „osobliwość” – lub, bardziej dramatycznie, „wysadzają”.

Gdy osiągną tę osobliwość, równania nie będą już w stanie obliczyć przepływu płynu. Ale „kilka lat temu to, co ludzie byli w stanie zrobić, było bardzo, bardzo dalekie od [udowodnienia eksplozji]”, powiedział Charliego Feffermana, matematyk z Uniwersytetu Princeton.

Staje się to jeszcze bardziej skomplikowane, jeśli próbujesz modelować płyn, który ma lepkość (jak prawie wszystkie płyny w świecie rzeczywistym). Milionowa Nagroda Millennium od Clay Mathematics Institute czeka na każdego, kto udowodni, że podobne awarie występują w równaniach Naviera-Stokesa, uogólnieniu równań Eulera, które uwzględniają lepkość.

W 2013, Tomasz Hou, matematyk z California Institute of Technology i Guo Luo, obecnie na Uniwersytecie Hang Seng w Hongkongu, zaproponował scenariusz, w którym równania Eulera prowadziłyby do osobliwości. Opracowali symulację komputerową płynu w cylindrze, którego górna połowa obracała się zgodnie z ruchem wskazówek zegara, a dolna połowa obracała się w kierunku przeciwnym do ruchu wskazówek zegara. Podczas przeprowadzania symulacji bardziej skomplikowane prądy zaczęły poruszać się w górę i w dół. To z kolei doprowadziło do dziwnego zachowania wzdłuż granicy cylindra, gdzie spotykały się przeciwne strumienie. Wirowość płynu — miara rotacji — rosła tak szybko, że wydawało się, że wybuchnie.

Praca Hou i Luo była sugestywna, ale nie była prawdziwym dowodem. To dlatego, że komputer nie jest w stanie obliczyć nieskończonych wartości. Może być bardzo blisko dostrzeżenia osobliwości, ale tak naprawdę nie może jej osiągnąć — co oznacza, że ​​rozwiązanie może być bardzo dokładne, ale nadal jest to przybliżenie. Bez wsparcia w postaci dowodu matematycznego wartość wirowości może tylko wydawać się rosnąca do nieskończoności z powodu jakiegoś artefaktu symulacji. Rozwiązania mogą zamiast tego urosnąć do ogromnych liczb, zanim ponownie opadną.

Takie odwrócenia zdarzały się już wcześniej: symulacja wskazywałaby, że wartość w równaniach eksplodowała, tylko po to, by bardziej wyrafinowane metody obliczeniowe wykazały inaczej. „Te problemy są tak delikatne, że droga jest zaśmiecona wrakami poprzednich symulacji” – powiedział Fefferman. W rzeczywistości w ten sposób Hou rozpoczął swoją pracę w tej dziedzinie: kilka z jego wcześniejszych wyników obaliło powstawanie hipotetycznych osobliwości.

Mimo to, kiedy on i Luo opublikowali swoje rozwiązanie, większość matematyków uważała, że ​​jest to bardzo prawdopodobne, że jest to prawdziwa osobliwość. „To było bardzo skrupulatne, bardzo precyzyjne” – powiedział Władimir Swierak, matematyk z University of Minnesota. „Naprawdę zadali sobie wiele trudu, aby ustalić, że jest to prawdziwy scenariusz”. Późniejsza praca Elgindiego, Sveraka i innych tylko umocnił to przekonanie.

Ale dowód był nieuchwytny. — Widziałeś bestię — powiedział Fefferman. „Potem próbujesz to uchwycić”. Oznaczało to pokazanie, że przybliżone rozwiązanie, które Hou i Luo tak dokładnie symulowali, jest w pewnym sensie matematycznym bardzo, bardzo bliskie dokładnemu rozwiązaniu równań.

Teraz, dziewięć lat po pierwszej obserwacji, Hou i jego były doktorant Jiajie Chen w końcu udało się udowodnić istnienie tej pobliskiej osobliwości.

Przeprowadzka do krainy samopodobnej

Hou, do którego później dołączył Chen, wykorzystał fakt, że po bliższej analizie przybliżone rozwiązanie z 2013 roku wydawało się mieć specjalną strukturę. W miarę jak równania ewoluowały w czasie, rozwiązanie wyświetlało tak zwany samopodobny wzór: jego kształt później wyglądał bardzo podobnie do wcześniejszego kształtu, tylko przeskalowany w określony sposób.

W rezultacie matematycy nie musieli próbować patrzeć na samą osobliwość. Zamiast tego mogli badać to pośrednio, skupiając się na wcześniejszym punkcie w czasie. Przybliżając tę ​​część rozwiązania we właściwym tempie — określonym na podstawie samopodobnej struktury rozwiązania — mogli modelować, co stanie się później, w tym w samej osobliwości.

Kilka lat zajęło im znalezienie analogii do scenariusza wybuchu z 2013 roku. (Na początku tego roku inny zespół matematyków, w skład którego wchodził Buckmaster, zastosował różne metody znaleźć podobne przybliżone rozwiązanie. Obecnie używają tego rozwiązania do opracowania niezależnego dowodu na powstawanie osobliwości.)

Dysponując przybliżonym samopodobnym rozwiązaniem, Hou i Chen musieli wykazać, że w pobliżu istnieje dokładne rozwiązanie. Z matematycznego punktu widzenia jest to równoznaczne z udowodnieniem, że ich przybliżone samopodobne rozwiązanie jest stabilne — że nawet gdybyś je lekko zaburzył, a następnie rozwinął równania, zaczynając od tych zaburzonych wartości, nie byłoby sposobu na ucieczkę z małego sąsiedztwa wokół przybliżone rozwiązanie. „To jak czarna dziura” — powiedział Hou. „Jeśli zaczniesz od profilu w pobliżu, zostaniesz wciągnięty”.

Ale posiadanie ogólnej strategii było tylko jednym krokiem w kierunku rozwiązania. „Wybredne szczegóły mają znaczenie”, powiedział Fefferman. Gdy Hou i Chen spędzili kilka następnych lat na opracowywaniu tych szczegółów, odkryli, że ponownie muszą polegać na komputerach — ale tym razem w zupełnie nowy sposób.

Podejście hybrydowe

Jednym z ich pierwszych wyzwań było ustalenie dokładnego stwierdzenia, które musieli udowodnić. Chcieli pokazać, że jeśli wezmą dowolny zestaw wartości zbliżonych do ich przybliżonego rozwiązania i wstawią go do równań, wynik nie będzie w stanie zabłądzić daleko. Ale co to znaczy, że dane wejściowe są „bliskie” rozwiązaniu przybliżonemu? Musieli to określić w stwierdzeniu matematycznym — ale istnieje wiele sposobów definiowania pojęcia odległości w tym kontekście. Aby ich dowód zadziałał, musieli wybrać właściwy.

„Musi mierzyć różne efekty fizyczne” – powiedział Rafaela de la Llave, matematyk z Georgia Institute of Technology. „Dlatego należy go wybrać przy głębokim zrozumieniu problemu”.

Kiedy już mieli właściwy sposób na opisanie „bliskości”, Hou i Chen musieli udowodnić to stwierdzenie, które sprowadzało się do skomplikowanej nierówności obejmującej składniki zarówno z przeskalowanych równań, jak i przybliżonego rozwiązania. Matematycy musieli upewnić się, że wartości wszystkich tych terminów równoważą się do czegoś bardzo małego: jeśli jedna wartość okazała się duża, inne wartości musiały być ujemne lub trzymane w ryzach.

„Jeśli zrobisz coś trochę za dużego lub trochę za małego, wszystko się psuje” – powiedział Javiera Gómeza-Serrano, matematyk z Brown University. „Więc jest to bardzo, bardzo ostrożna, delikatna praca”.

„To naprawdę zacięta walka” — dodał Elgindi.

Aby uzyskać ścisłe granice, których potrzebowali na wszystkich tych różnych warunkach, Hou i Chen podzielili nierówność na dwie główne części. Pierwszą część mogli wykonać ręcznie, wykorzystując techniki, w tym jedną sięgającą XVIII wieku, kiedy to francuski matematyk Gaspard Monge poszukiwał optymalnego sposobu transportu ziemi do budowy fortyfikacji dla armii napoleońskiej. „Takie rzeczy robiono już wcześniej, ale uznałem za uderzające, że [Hou i Chen] wykorzystali to do tego” – powiedział Fefferman.

To pozostawiło drugą część nierówności. Zwalczanie go wymagałoby pomocy komputera. Na początek trzeba było wykonać tak wiele obliczeń i wymagać tak dużej precyzji, że „ilość pracy, którą trzeba wykonać z ołówkiem i papierem, byłaby oszałamiająca” — powiedział de la Llave. Aby zrównoważyć różne warunki, matematycy musieli wykonać szereg problemów optymalizacyjnych, które są stosunkowo łatwe dla komputerów, ale niezwykle czasochłonne dla ludzi. Niektóre wartości zależały również od wielkości z przybliżonego rozwiązania; ponieważ obliczono to za pomocą komputera, prostsze było również użycie komputera do wykonania tych dodatkowych obliczeń.

„Jeśli spróbujesz ręcznie wykonać niektóre z tych szacunków, prawdopodobnie w pewnym momencie przeszacujesz, a potem przegrasz” – powiedział Gómez-Serrano. „Liczby są tak małe i ciasne… a margines jest niewiarygodnie cienki”.

Ale ponieważ komputery nie mogą manipulować nieskończoną liczbą cyfr, nieuchronnie pojawiają się drobne błędy. Hou i Chen musieli dokładnie śledzić te błędy, aby upewnić się, że nie przeszkadzają one w dalszej części równoważenia.

Ostatecznie udało im się znaleźć granice dla wszystkich terminów, kończąc dowód: równania rzeczywiście dały osobliwość.

Dowód przez komputer

Pozostaje otwarte, czy bardziej skomplikowane równania - równania Eulera bez obecności cylindrycznej granicy i równania Naviera-Stokesa - mogą rozwinąć osobliwość. „Ale [ta praca] przynajmniej daje mi nadzieję” — powiedział Hou. „Widzę drogę naprzód, sposób, by być może ostatecznie rozwiązać cały problem milenijny”.

W międzyczasie Buckmaster i Gómez-Serrano pracują nad własnym dowodem wspomaganym komputerowo — który, jak mają nadzieję, będzie bardziej ogólny, a zatem będzie w stanie rozwiązać nie tylko problem, który rozwiązali Hou i Chen, ale także dziesiątki innych.

Wysiłki te wyznaczają rosnący trend w dziedzinie dynamiki płynów: wykorzystanie komputerów do rozwiązywania ważnych problemów.

„W wielu różnych dziedzinach matematyki zdarza się to coraz częściej” – powiedział Zuzanna Friedlander, matematyk z University of Southern California.

Ale w mechanice płynów dowody wspomagane komputerowo są wciąż stosunkowo nową techniką. W rzeczywistości, jeśli chodzi o stwierdzenia dotyczące powstawania osobliwości, dowód Hou i Chen jest pierwszym tego rodzaju: poprzednie dowody wspomagane komputerowo były w stanie rozwiązać problemy z zabawkami tylko w tym obszarze.

Takie dowody są nie tyle kontrowersyjne, co „kwestią gustu”, powiedział Piotr Konstantyn z Uniwersytetu Princeton. Matematycy na ogół zgadzają się, że dowód musi przekonać innych matematyków, że jakaś linia rozumowania jest poprawna. Ale wielu twierdzi, że powinno to również poprawić ich zrozumienie, dlaczego dane stwierdzenie jest prawdziwe, zamiast po prostu potwierdzać, że jest poprawne. „Czy uczymy się czegoś zasadniczo nowego, czy po prostu znamy odpowiedź na pytanie?” — powiedział Elgindi. „Jeśli postrzegasz matematykę jako sztukę, to nie jest to tak przyjemne estetycznie”.

„Komputer może pomóc. To jest wspaniałe. Daje mi wgląd. Ale to nie daje mi pełnego zrozumienia” – dodał Constantin. „Zrozumienie pochodzi od nas”.

Ze swojej strony Elgindi nadal ma nadzieję na wypracowanie alternatywnego dowodu wysadzenia całkowicie ręcznie. „Ogólnie cieszę się, że to istnieje” — powiedział o pracy Hou i Chena. „Ale traktuję to bardziej jako motywację, aby spróbować zrobić to w sposób mniej zależny od komputera”.

Inni matematycy postrzegają komputery jako istotne nowe narzędzie, które umożliwi zaatakowanie wcześniej trudnych problemów. „Teraz praca to już nie tylko papier i ołówek” — powiedział Chen. „Masz możliwość użycia czegoś potężniejszego”.

Według niego i innych (w tym Elgindiego, pomimo jego osobistych preferencji do ręcznego pisania dowodów), istnieje duże prawdopodobieństwo, że jedynym sposobem rozwiązania dużych problemów w dynamice płynów — to znaczy problemów obejmujących coraz bardziej skomplikowane równania — może być poleganie na mocno na pomocy komputera. „Wydaje mi się, że próba zrobienia tego bez intensywnego korzystania z dowodów wspomaganych komputerowo jest jak związanie jednej lub dwóch rąk za plecami” – powiedział Fefferman.

Jeśli tak się stanie i „nie masz żadnego wyboru”, powiedział Elgindi, „to ludzie… tacy jak ja, którzy powiedzieliby, że jest to nieoptymalne, powinni być cicho”. Oznaczałoby to również, że więcej matematyków musiałoby zacząć uczyć się umiejętności potrzebnych do pisania wspomaganych komputerowo dowodów – coś, co, miejmy nadzieję, zainspiruje praca Hou i Chena. „Myślę, że było wielu ludzi, którzy po prostu czekali, aż ktoś rozwiąże taki problem, zanim zainwestują swój czas w to podejście” — powiedział Buckmaster.

To powiedziawszy, jeśli chodzi o debaty na temat tego, w jakim stopniu matematycy powinni polegać na komputerach, „nie chodzi o to, że musisz wybrać stronę”, powiedział Gómez-Serrano. „Dowód [Hou i Chen] nie zadziałałby bez analizy, a dowód nie zadziałałby bez pomocy komputera. … Myślę, że wartość polega na tym, że ludzie mogą mówić tymi dwoma językami”.

W związku z tym de la Llave powiedział: „w mieście jest nowa gra”.

Znak czasu:

Więcej z Magazyn ilościowy