Комп’ютерний доказ «підриває» багатовікові рідинні рівняння PlatoBlockchain Data Intelligence. Вертикальний пошук. Ai.

Комп’ютерний доказ «підриває» багатовікові рівняння рідини

Вступ

Століттями математики намагалися зрозуміти та змоделювати рух рідин. Рівняння, які описують, як брижі утворюють складки на поверхні ставка, також допомогли дослідникам передбачити погоду, сконструювати кращі літаки та охарактеризувати, як кров тече через кровоносну систему. Ці рівняння оманливо прості, якщо їх написати правильною математичною мовою. Однак їх рішення настільки складні, що розібратися навіть у основних питаннях про них може бути надзвичайно важко.

Можливо, найдавніше та найвидатніше з цих рівнянь, сформульоване Леонгардом Ейлером понад 250 років тому, описує потік ідеальної нестисливої ​​рідини: рідини без в’язкості або внутрішнього тертя, яку неможливо натиснути в менший об’єм. «Майже всі нелінійні рівняння рідини є начебто похідними від рівнянь Ейлера», — сказав Тарек Елгінді, математик в Університеті Дьюка. «Вони перші, можна сказати».

Проте багато чого залишається невідомим про рівняння Ейлера — зокрема, чи завжди вони є точною моделлю потоку ідеальної рідини. Однією з головних проблем у динаміці рідини є з’ясування, чи рівняння коли-небудь виявляють невдачу, виводячи безглузді значення, які роблять їх нездатними передбачити майбутні стани рідини.

Математики давно підозрюють, що існують початкові умови, які спричиняють порушення рівнянь. Але вони не змогли цього довести.

In препринт опубліковані в Інтернеті минулого місяця, пара математиків показала, що певна версія рівнянь Ейлера справді іноді не дає результатів. Доказ знаменує великий прорив — і хоча він не повністю вирішує проблему для більш загальної версії рівнянь, він дає надію, що таке рішення нарешті доступне. «Це приголомшливий результат», - сказав Трістан Бакмастер, математик з Мерілендського університету, який не брав участі в роботі. «У літературі немає результатів такого роду».

Є лише одна заковика.

177-сторінковий доказ — результат десятирічної дослідницької програми — значно використовує комп’ютери. Можливо, це ускладнює перевірку іншим математикам. (Насправді вони все ще займаються цим, хоча багато експертів вважають, що нова робота виявиться правильною.) Це також змушує їх рахуватися з філософськими питаннями про те, що таке «доказ» і що воно буде означає, що єдиним життєздатним способом вирішення таких важливих питань у майбутньому є за допомогою комп’ютерів.

Спостереження за звіром

У принципі, якщо ви знаєте розташування та швидкість кожної частинки в рідині, рівняння Ейлера повинні мати можливість передбачити, як рідина буде розвиватися за весь час. Але математики хочуть знати, чи це насправді так. Можливо, у деяких ситуаціях рівняння працюватимуть так, як очікувалося, створюючи точні значення стану рідини в будь-який момент, лише для того, щоб одне з цих значень раптово різко зросло до нескінченності. У цей момент рівняння Ейлера, як кажуть, викликають «сингулярність» — або, що більш драматично, «вибухають».

Як тільки вони досягнуть цієї сингулярності, рівняння більше не зможуть обчислити потік рідини. Але «кілька років тому те, що люди могли зробити, було дуже, дуже далеко від [доведення розриву]», — сказав Чарлі Фефферман, математик Прінстонського університету.

Це стає ще складнішим, якщо ви намагаєтеся змоделювати рідину, яка має в’язкість (як майже всі реальні рідини). Премія тисячоліття в розмірі мільйон доларів від Математичного інституту Клея чекає на кожного, хто зможе довести, чи трапляються подібні збої в рівняннях Нав’є-Стокса, узагальненні рівнянь Ейлера, що враховує в’язкість.

У 2013, Томас Хоу, математик Каліфорнійського технологічного інституту, і Го Луо, який зараз працює в Університеті Ханг Сенг у Гонконзі, запропонував сценарій, за яким рівняння Ейлера призведуть до сингулярності. Вони розробили комп’ютерне моделювання рідини в циліндрі, верхня половина якого обертається за годинниковою стрілкою, а нижня – проти годинникової стрілки. Коли вони запускали симуляцію, більш складні течії почали рухатися вгору та вниз. Це, у свою чергу, призвело до дивної поведінки вздовж межі циліндра, де зустрічалися протилежні потоки. Завихреність рідини — міра обертання — зростала настільки швидко, що, здавалося, вона була готова вибухнути.

Робота Хоу і Луо була навідною, але не справжнім доказом. Це тому, що комп’ютер не може обчислити нескінченні значення. Він може наблизитися до того, щоб побачити сингулярність, але насправді не може її досягти — це означає, що рішення може бути дуже точним, але воно все ще є наближенням. Без підтримки математичних доказів значення завихреності могло б лише здаватися, що воно зростає до нескінченності через якийсь артефакт симуляції. Натомість рішення можуть зрости до величезних кількостей, перш ніж знову вщухнути.

Такі зміни траплялися й раніше: симуляція вказувала на те, що значення в рівняннях вибухнуло, лише для більш складних обчислювальних методів, щоб показати протилежне. «Ці проблеми настільки делікатні, що дорога всіяна уламками попередніх симуляцій», — сказав Фефферман. Власне, саме так Хоу почав працювати в цій галузі: кілька його попередніх результатів спростували утворення гіпотетичних сингулярностей.

Проте, коли вони з Ло опублікували своє рішення, більшість математиків вважали, що це дуже ймовірно справжня сингулярність. «Це було дуже скрупульозно, дуже точно», — сказав Володимир Сверак, математик в Університеті Міннесоти. «Вони дійсно доклали чимало зусиль, щоб встановити, що це реальний сценарій». Подальша робота Елгінді, Сверака та ін тільки зміцнив це переконання.

Але доказ був невловимий. «Ви помітили звіра», — сказав Фефферман. «Тоді ви спробуйте це захопити». Це означало показати, що наближене рішення, яке Хоу і Луо так ретельно змоделювали, у конкретному математичному сенсі дуже, дуже близько до точного розв’язку рівнянь.

Тепер, через дев’ять років після того першого побачення, Хоу та його колишній аспірант Цзяцзе Чень нарешті вдалося довести існування цієї близької сингулярності.

Переїзд на самоподібну землю

Хоу, до якого пізніше приєднався Чень, скористався тим фактом, що при детальнішому аналізі наближене рішення 2013 року, здавалося, мало особливу структуру. У міру того, як рівняння змінювалися з часом, розв’язок демонстрував так звану самоподібну структуру: її форма згодом виглядала дуже схожою на попередню форму, тільки перемасштабована певним чином.

У результаті математикам не потрібно було намагатися поглянути на саму сингулярність. Натомість вони могли вивчати це опосередковано, зосереджуючись на більш ранньому моменті часу. Збільшуючи цю частину рішення з правильною швидкістю — визначеною на основі самоподібної структури рішення — вони могли моделювати те, що станеться пізніше, включно з самою сингулярністю.

Їм знадобилося кілька років, щоб знайти самоподібний аналог сценарію вибуху 2013 року. (На початку цього року інша команда математиків, до якої входив Бакмастер, використовувала різні методи, щоб знайти подібне наближене рішення. Зараз вони використовують це рішення для розробки незалежного доказу формування сингулярності.)

Маючи на руках наближений самоподібний розв’язок, Хоу та Чен мали показати, що поруч існує точний розв’язок. З математичної точки зору це еквівалентно доведенню того, що їхній наближений самоподібний розв’язок є стабільним — що навіть якщо ви трохи спотворите його, а потім розробите рівняння, починаючи з цих збурених значень, не буде жодного способу уникнути невеликого сусідства навколо наближене рішення. "Це як чорна діра", - сказав Хоу. «Якщо ви почнете з профілю поруч, вас затягне».

Але наявність загальної стратегії була лише одним кроком до вирішення. «Метушливі деталі мають значення», — сказав Фефферман. Протягом наступних кількох років Хоу та Чен з’ясували, що їм знову доводиться покладатися на комп’ютери, але цього разу в абсолютно новий спосіб.

Гібридний підхід

Серед їхніх перших труднощів було з’ясувати точне твердження, яке вони мали довести. Вони хотіли показати, що якби вони взяли будь-який набір значень, близьких до їхнього наближеного рішення, і включили його в рівняння, результат не міг би заблукати далеко. Але що це означає, якщо вхідний сигнал «близький» до приблизного рішення? Їм довелося вказати це в математичному формулюванні, але існує багато способів визначити поняття відстані в цьому контексті. Щоб їхній доказ спрацював, їм потрібно було вибрати правильний.

«Це має вимірювати різні фізичні ефекти», — сказав Рафаель де ла Льяве, математик Технологічного інституту Джорджії. «Тож його потрібно обирати, глибоко розуміючи проблему».

Коли вони знайшли правильний спосіб описати «близькість», Хоу і Чен повинні були довести це твердження, яке зводилося до складної нерівності, що включає члени як із змінених рівнянь, так і з наближеного розв’язку. Математики повинні були переконатися, що значення всіх цих термінів збалансовані до чогось дуже малого: якщо одне значення виявляється великим, інші значення повинні бути від’ємними або триматися під контролем.

«Якщо ви робите щось занадто велике або занадто маленьке, все вийде з ладу», — сказав він Хав'єр Гомес-Серрано, математик з Університету Брауна. «Тож це дуже, дуже обережна, делікатна робота».

«Це справді запекла боротьба», — додав Елгінді.

Щоб отримати тісні межі, які їм потрібні були для всіх цих різних умов, Хоу і Чень розбили нерівність на дві основні частини. Вони могли подбати про першу частину вручну, використовуючи техніку, включно з технікою, яка датується 18 століттям, коли французький математик Гаспар Монж шукав оптимальний спосіб транспортування ґрунту для будівництва укріплень для армії Наполеона. «Подібні речі робили раніше, але я вважаю вражаючим, що [Хоу і Чень] використовували це для цього», — сказав Фефферман.

Осталася друга частина нерівності. Для вирішення цього знадобиться допомога комп’ютера. По-перше, потрібно було виконати стільки обчислень і стільки точності, що «обсяг роботи, яку вам доведеться виконати з олівцем і папером, був би приголомшливим», — сказав де ла Ллав. Щоб збалансувати різні терміни, математикам довелося виконати серію задач оптимізації, які відносно легкі для комп’ютерів, але надзвичайно трудомісткі для людей. Деякі значення також залежали від величин з наближеного розчину; оскільки це було обчислено за допомогою комп’ютера, було простіше також використовувати комп’ютер для виконання цих додаткових обчислень.

«Якщо ви спробуєте зробити деякі з цих оцінок вручну, ви, ймовірно, в якийсь момент переоціните їх, а потім програєте», — сказав Гомес-Серрано. «Цифри такі крихітні та вузькі… а маржа неймовірно мала».

Але оскільки комп’ютери не можуть працювати з нескінченною кількістю цифр, неминуче виникають крихітні помилки. Хоу і Чен повинні були ретельно відстежувати ці помилки, щоб переконатися, що вони не заважають решті балансування.

Зрештою, вони змогли знайти межі для всіх членів, завершивши доказ: рівняння справді породили сингулярність.

Доказ за допомогою комп’ютера

Залишається відкритим, чи можуть більш складні рівняння — рівняння Ейлера без присутності циліндричної межі та рівняння Нав’є-Стокса — розвивати сингулярність. «Але [ця робота] принаймні дає мені надію», — сказав Хоу. «Я бачу шлях вперед, спосіб, можливо, врешті-решт вирішити повну проблему тисячоліття».

Тим часом Бакмастер і Гомес-Серрано працюють над власним комп’ютерним доказом — вони сподіваються, що він буде більш загальним і, отже, здатним вирішити не лише проблему, яку вирішили Хоу та Чень, а й безліч інших.

Ці зусилля знаменують зростаючу тенденцію в галузі динаміки рідин: використання комп’ютерів для вирішення важливих проблем.

«У ряді різних галузей математики це трапляється все частіше», — сказав Сьюзан Фрідлендер, математик Університету Південної Каліфорнії.

Але в механіці рідин комп’ютерні докази все ще є відносно новою технікою. Насправді, коли справа доходить до тверджень про формування сингулярності, доказ Хоу і Чена є першим у своєму роді: попередні комп’ютерні докази могли вирішувати лише проблеми іграшок у цій області.

Такі докази не стільки суперечливі, скільки «справа смаку». Петро Костянтин Прінстонського університету. Математики загалом погоджуються, що доказ має переконати інших математиків у правильності деяких міркувань. Але, на думку багатьох, це також має покращити їхнє розуміння того, чому певне твердження є істинним, а не просто надати підтвердження його правильності. «Чи дізнаємося ми щось принципово нове, чи просто знаємо відповідь на запитання?» – сказав Елгінді. «Якщо розглядати математику як мистецтво, то це не так естетично».

«Комп’ютер може допомогти. Це прекрасно. Це дає мені розуміння. Але це не дає мені повного розуміння», – додав Костянтин. «Розуміння йде від нас».

Зі свого боку, Елгінді все ще сподівається розробити альтернативний доказ вибуху повністю вручну. «Я загалом радий, що це існує», — сказав він про роботу Хоу та Ченя. «Але я сприймаю це більше як мотивацію спробувати зробити це менш залежним від комп’ютера способом».

Інші математики розглядають комп’ютери як життєво важливий новий інструмент, який дозволить атакувати раніше нерозв’язні проблеми. «Тепер робота — це не лише папір і олівець», — сказав Чень. «У вас є можливість використовувати щось більш потужне».

За його словами та іншими (включаючи Елгінді, незважаючи на його особисту перевагу писати докази вручну), існує хороша ймовірність того, що єдиний спосіб вирішити великі проблеми в динаміці рідини — тобто проблеми, які включають дедалі складніші рівняння — може полягати в тому, щоб покладатися на багато в комп’ютерній допомозі. «Мені здається, що спроба зробити це, не вдаючись до комп’ютерних доказів, схожа на зв’язування однієї чи, можливо, двох рук за спиною», — сказав Фефферман.

Якщо це все-таки так і «у вас не буде вибору», - сказав Елгінді, «тоді люди... такі як я, які скажуть, що це неоптимально, повинні замовкнути». Це також означало б, що більше математиків повинні будуть почати вивчати навички, необхідні для написання доказів за допомогою комп’ютера — те, на що робота Хоу і Чена, сподіваюся, надихне. «Я думаю, що було багато людей, які просто чекали, що хтось вирішить таку проблему, перш ніж вкладати власний час у цей підхід», — сказав Бакмастер.

Проте, коли справа доходить до дебатів про те, якою мірою математики повинні покладатися на комп’ютери, «справа не в тому, що вам потрібно вибирати сторону», — сказав Гомес-Серрано. «Доказ [Хоу і Чена] не працював би без аналізу, а доказ не працював би без допомоги комп’ютера. … Я думаю, що цінність полягає в тому, що люди можуть говорити двома мовами».

При цьому де ла Льяв сказав: «У місті нова гра».

Часова мітка:

Більше від Квантамагазин