הוכחת מחשב 'מפוצצת' משוואות נוזלים בנות מאות שנים PlatoBlockchain Data Intelligence. חיפוש אנכי. איי.

הוכחת מחשב 'מפוצצת' משוואות נוזלים בנות מאות שנים

מבוא

במשך מאות שנים, מתמטיקאים ביקשו להבין ולדגמן את תנועת הנוזלים. המשוואות המתארות כיצד אדוות מקמטות את פני הבריכה עזרו גם לחוקרים לחזות את מזג האוויר, לתכנן מטוסים טובים יותר ולאפיין את האופן שבו הדם זורם דרך מערכת הדם. המשוואות האלה פשוטות בצורה מטעה כשהן כתובות בשפה המתמטית הנכונה. עם זאת, הפתרונות שלהם כל כך מורכבים עד שקשה מאוד להבין אפילו שאלות בסיסיות לגביהם.

אולי העתיק והבולט מבין המשוואות הללו, שנוסח על ידי לאונרד אוילר לפני יותר מ-250 שנה, מתאר זרימה של נוזל אידיאלי, בלתי ניתן לדחיסה: נוזל ללא צמיגות, או חיכוך פנימי, שלא ניתן לכפות עליו נפח קטן יותר. "כמעט כל משוואות הנוזל הלא ליניאריות נגזרות ממש ממשוואות אוילר", אמר טארק אלגינדי, מתמטיקאי באוניברסיטת דיוק. "הם הראשונים, אפשר לומר."

עם זאת, הרבה לא ידוע על משוואות אוילר - כולל האם הן תמיד מודל מדויק של זרימת נוזלים אידיאלית. אחת הבעיות המרכזיות בדינמיקה של נוזלים היא להבין אם המשוואות אי פעם נכשלות, ומוציאות ערכים חסרי היגיון שהופכים אותם ללא מסוגלים לחזות את המצבים העתידיים של נוזל.

מתמטיקאים חשדו זה מכבר שקיימים תנאים ראשוניים שגורמים להתפרקות המשוואות. אבל הם לא הצליחו להוכיח זאת.

In הדפס מקדים פורסם באינטרנט בחודש שעבר, זוג מתמטיקאים הראו שגרסה מסוימת של משוואות אוילר אכן נכשלת לפעמים. ההוכחה מסמנת פריצת דרך גדולה - ולמרות שהיא לא פותרת לחלוטין את הבעיה עבור הגרסה הכללית יותר של המשוואות, היא מציעה תקווה שפתרון כזה נמצא סוף סוף בהישג יד. "זו תוצאה מדהימה", אמר טריסטן באקמאסטר, מתמטיקאי באוניברסיטת מרילנד שלא היה מעורב בעבודה. "אין תוצאות מסוג זה בספרות."

יש רק מלכוד אחד.

ההוכחה בת 177 העמודים - תוצאה של תוכנית מחקר בת עשור - עושה שימוש משמעותי במחשבים. זה ללא ספק מקשה על מתמטיקאים אחרים לאמת זאת. (למעשה, הם עדיין בתהליך לעשות זאת, אם כי מומחים רבים מאמינים שהעבודה החדשה תתברר כנכונה.) היא גם מאלצת אותם להתחשב בשאלות פילוסופיות לגבי מהי "הוכחה" ומה היא תהיה. כלומר, אם הדרך הישימה היחידה לפתור שאלות חשובות כאלה בהמשך היא בעזרת מחשבים.

לראות את החיה

באופן עקרוני, אם אתה יודע את המיקום והמהירות של כל חלקיק בנוזל, משוואות אוילר אמורות להיות מסוגלות לחזות כיצד הנוזל יתפתח לכל עת. אבל מתמטיקאים רוצים לדעת אם זה באמת המקרה. אולי במצבים מסוימים, המשוואות יתנהלו כצפוי, וייצרו ערכים מדויקים למצב הנוזל בכל רגע נתון, רק שאחד מאותם ערכים יזנק פתאום עד אינסוף. בשלב זה, אומרים שמשוואות אוילר יוצרות "ייחוד" - או, באופן דרמטי יותר, "לפוצץ".

ברגע שהם פגעו בייחוד הזה, המשוואות לא יוכלו עוד לחשב את זרימת הנוזל. אבל "לפני כמה שנים, מה שאנשים היו מסוגלים לעשות לא היה מאוד מאוד רחוק [להוכיח פיצוץ]", אמר צ'רלי פפרמן, מתמטיקאי באוניברסיטת פרינסטון.

זה נעשה אפילו יותר מסובך אם אתה מנסה ליצור מודל של נוזל בעל צמיגות (כפי שכמעט כל הנוזלים בעולם האמיתי עושים). פרס מילניום בסך מיליון דולר ממכון קליי מתמטיקה ממתין לכל מי שיכול להוכיח האם כשלים דומים מתרחשים במשוואות נאוויאר-סטוקס, הכללה של משוואות אוילר המסבירות את הצמיגות.

ב2013, תומאס הו, מתמטיקאי במכון הטכנולוגי של קליפורניה, ו גו לו לו, כעת באוניברסיטת האנג סנג בהונג קונג, הציע תרחיש שבו משוואות אוילר יובילו לייחודיות. הם פיתחו הדמיית מחשב של נוזל בצילינדר שחציו העליון הסתחרר בכיוון השעון ואילו החצי התחתון שלו הסתחרר נגד כיוון השעון. בזמן שהריצו את הסימולציה, זרמים מסובכים יותר החלו לנוע מעלה ומטה. זה, בתורו, הוביל להתנהגות מוזרה לאורך גבול הגליל שבו נפגשו זרימות מנוגדות. מערבולת הנוזל - מידה של סיבוב - גדלה כל כך מהר עד שנראה היה שהוא עומד להתפוצץ.

עבודתם של הו ולאו הייתה מרמזת, אבל לא הוכחה אמיתית. זה בגלל שאי אפשר למחשב לחשב אינסוף ערכים. זה יכול להתקרב מאוד למראה ייחוד, אבל הוא לא יכול להגיע אליו בפועל - כלומר הפתרון עשוי להיות מדויק מאוד, אבל זה עדיין קירוב. ללא גיבוי של הוכחה מתמטית, הערך של המערבולת עשוי להיראות רק הולך וגדל עד אינסוף בגלל חפץ כלשהו של הסימולציה. במקום זאת, הפתרונות עשויים לגדול למספרים עצומים לפני ששוב ישמעו.

היפוכים כאלה קרו בעבר: סימולציה תצביע על כך שערך במשוואות התפוצץ, רק כדי ששיטות חישוב מתוחכמות יותר יראו אחרת. "הבעיות האלה כל כך עדינות שהכביש עמוס בהריסות של סימולציות קודמות", אמר פפרמן. למעשה, כך הוא התחיל בתחום הזה: כמה מהתוצאות הקודמות שלו הפריכו את היווצרותן של ייחודיות היפותטיות.

ובכל זאת, כשהוא ולואו פרסמו את הפתרון שלהם, רוב המתמטיקאים חשבו שזה סביר מאוד שזה ייחוד אמיתי. "זה היה מאוד קפדני, מאוד מדויק", אמר ולדימיר סברק, מתמטיקאי באוניברסיטת מינסוטה. "הם באמת עשו מאמצים רבים כדי לקבוע שזהו תרחיש אמיתי". עבודה שלאחר מכן מאת אלגינדי, סברק ואחרים רק חיזק את ההרשעה הזו.

אבל הוכחה הייתה חמקמקה. "ראית את החיה," אמר פפרמן. "אז אתה מנסה ללכוד את זה." פירוש הדבר היה להראות שהפתרון המשוער שהאו ולואו דימו בקפידה רבה, במובן מתמטי ספציפי, קרוב מאוד מאוד לפתרון מדויק של המשוואות.

כעת, תשע שנים לאחר המראה הראשון, הו ותלמידו לשעבר ג'יאג'י צ'ן סוף סוף הצליחו להוכיח את קיומה של אותה ייחוד קרוב.

המעבר לארץ דומה לעצמה

הו, שאליה הצטרף מאוחר יותר חן, ניצלה את העובדה שבניתוח מעמיק יותר נראה שלפתרון המשוער מ-2013 יש מבנה מיוחד. ככל שהמשוואות התפתחו עם הזמן, הפתרון הציג את מה שנקרא תבנית דומה לעצמה: צורתו מאוחר יותר נראתה דומה מאוד לצורתו הקודמת, רק גודלה מחדש בצורה ספציפית.

כתוצאה מכך, המתמטיקאים לא היו צריכים לנסות להסתכל על הסינגולריות עצמה. במקום זאת, הם יכלו ללמוד זאת בעקיפין על ידי התמקדות בנקודת זמן מוקדמת יותר. על ידי התקרבות לחלק הזה של הפתרון בקצב הנכון - שנקבע על סמך המבנה הדומה לעצמו של הפתרון - הם יכולים לדגמן את מה שיקרה בהמשך, כולל הייחודיות עצמה.

לקח להם כמה שנים למצוא אנלוגי דומה לתרחיש הפיצוץ של 2013. (מוקדם יותר השנה, צוות נוסף של מתמטיקאים, שכלל את Buckmaster, השתמש בשיטות שונות כדי למצוא פתרון משוער דומה. כרגע הם משתמשים בפתרון הזה כדי לפתח הוכחה עצמאית להיווצרות ייחוד.)

עם פתרון דומה עצמי משוער ביד, הו וצ'ן היו צריכים להראות שקיים פתרון מדויק בקרבת מקום. מבחינה מתמטית, זה שווה ערך להוכחה שהפתרון הדומה העצמי המשוער שלהם יציב - שגם אם היית מפריע לו מעט ואז מפתח את המשוואות החל מהערכים המופרעים האלה, לא תהיה דרך לברוח משכונה קטנה מסביב ל- פתרון משוער. "זה כמו חור שחור," אמר הו. "אם תתחיל עם פרופיל קרוב, אתה תישאב פנימה."

אבל אסטרטגיה כללית הייתה רק צעד אחד לקראת הפתרון. "פרטים קפדניים חשובים," אמר פפרמן. בעוד הו וצ'ן בילו את השנים הבאות בפיתוח הפרטים הללו, הם גילו שהם נאלצו להסתמך על מחשבים שוב - אבל הפעם בצורה חדשה לגמרי.

גישה היברידית

בין האתגרים הראשונים שלהם היה להבין את ההצהרה המדויקת שהם צריכים להוכיח. הם רצו להראות שאם הם לוקחים סט ערכים קרוב לפתרון המשוער שלהם ומחברים אותו למשוואות, הפלט לא יוכל לסטות רחוק. אבל מה המשמעות של קלט להיות "קרוב" לפתרון המשוער? הם היו צריכים לציין זאת בהצהרה מתמטית - אך ישנן דרכים רבות להגדיר את מושג המרחק בהקשר זה. כדי שההוכחה שלהם תעבוד, הם היו צריכים לבחור את ההוכחה הנכונה.

"זה צריך למדוד השפעות פיזיות שונות," אמר רפאל דה לה לאבה, מתמטיקאי במכון הטכנולוגי של ג'ורג'יה. "אז צריך לבחור אותו תוך שימוש בהבנה עמוקה של הבעיה."

ברגע שהייתה להם הדרך הנכונה לתאר "קרבה", הו וצ'ן היו צריכים להוכיח את ההצהרה, שהסתכמה לאי שוויון מסובך הכולל מונחים הן מהמשוואות בקנה מידה מחדש והן מהפתרון המשוער. המתמטיקאים היו צריכים לוודא שהערכים של כל המונחים הללו מאוזנים למשהו קטן מאוד: אם ערך אחד בסופו של דבר היה גדול, ערכים אחרים היו צריכים להיות שליליים או לשמור על שליטה.

"אם אתה עושה משהו קצת גדול מדי או קצת קטן מדי, כל העניין מתקלקל," אמר חאבייר גומז-סראנו, מתמטיקאי באוניברסיטת בראון. "אז זו עבודה מאוד מאוד זהירה ועדינה."

"זה קרב עז באמת", הוסיף אלגינדי.

כדי להגיע לגבולות ההדוקים שהם היו צריכים בכל התנאים השונים האלה, האו וצ'ן שברו את אי השוויון לשני חלקים עיקריים. הם יכלו לטפל בחלק הראשון ביד, עם טכניקות כולל טכניקות שראשיתה במאה ה-18, כאשר המתמטיקאי הצרפתי גספרד מונגה חיפש דרך אופטימלית להובלת אדמה לבניית ביצורים עבור צבאו של נפוליאון. "דברים כאלה נעשו בעבר, אבל מצאתי שזה מדהים ש[Hou וצ'ן] השתמשו בזה בשביל זה", אמר פפרמן.

זה השאיר את החלק השני של אי השוויון. התמודדות עם זה תדרוש סיוע במחשב. בתור התחלה, היו כל כך הרבה חישובים שצריך לעשות, וכל כך הרבה דיוק נדרש, ש"כמות העבודה שתצטרך לעשות עם עיפרון ונייר תהיה מדהימה", אמר דה לה לאבה. כדי לגרום למונחים שונים להתאזן, המתמטיקאים היו צריכים לבצע סדרה של בעיות אופטימיזציה שהן קלות יחסית למחשבים אך גוזלות זמן רב עבור בני אדם. חלק מהערכים היו תלויים גם בכמויות מהפתרון המשוער; מכיוון שזה חושב באמצעות מחשב, היה יותר פשוט להשתמש גם במחשב כדי לבצע את החישובים הנוספים הללו.

"אם תנסה לבצע כמה מההערכות האלה באופן ידני, אתה כנראה הולך להעריך יתר על המידה בשלב מסוים, ואז אתה מפסיד," אמר גומז-סראנו. "המספרים כל כך זעירים וצפופים... והשוליים דקים להפליא."

אבל מכיוון שמחשבים לא יכולים לתפעל מספר אינסופי של ספרות, שגיאות זעירות מתרחשות בהכרח. הו וצ'ן נאלצו לעקוב בקפידה אחר השגיאות הללו, כדי לוודא שהן לא מפריעות להמשך פעולת האיזון.

בסופו של דבר, הם הצליחו למצוא גבולות לכל המונחים, והשלימו את ההוכחה: המשוואות אכן יצרו ייחוד.

הוכחה באמצעות מחשב

נותר פתוח אם משוואות מסובכות יותר - משוואות אוילר ללא נוכחות של גבול גלילי ומשוואות Navier-Stokes - יכולות לפתח ייחוד. "אבל [העבודה הזו] לפחות נותנת לי תקווה", אמר הו. "אני רואה דרך קדימה, דרך אולי אפילו לפתור את בעיית המילניום המלאה".

בינתיים, באקמאסטר וגומז-סראנו עובדים על הוכחה משלהם בעזרת מחשב - כזו שהם מקווים שתהיה כללית יותר, ולכן מסוגלת להתמודד לא רק עם הבעיה שהו וצ'ן פתרו, אלא גם עשרות אחרים.

מאמצים אלו מסמנים מגמה הולכת וגוברת בתחום הדינמיקה הנוזלית: שימוש במחשבים לפתרון בעיות חשובות.

"במספר תחומים שונים של מתמטיקה, זה מתרחש לעתים קרובות יותר ויותר", אמר סוזן פרידלנדר, מתמטיקאי באוניברסיטת דרום קליפורניה.

אבל במכניקת הזרימה, הוכחות בעזרת מחשב הן עדיין טכניקה חדשה יחסית. למעשה, כשמדובר בהצהרות על היווצרות ייחוד, ההוכחה של Hou וצ'ן היא הראשונה מסוגה: הוכחות קודמות בעזרת מחשב הצליחו להתמודד רק עם בעיות צעצוע באזור.

הוכחות כאלה אינן כל כך שנויות במחלוקת כמו "עניין של טעם", אמר פיטר קונסטנטין מאוניברסיטת פרינסטון. מתמטיקאים בדרך כלל מסכימים שהוכחה צריכה לשכנע מתמטיקאים אחרים שקו מחשבה כלשהו נכון. אבל, רבים טוענים, זה צריך גם לשפר את ההבנה שלהם מדוע הצהרה מסוימת נכונה, במקום פשוט לספק אימות לכך שהיא נכונה. "האם אנחנו לומדים משהו חדש ביסודו, או שאנחנו פשוט יודעים את התשובה לשאלה?" אמר אלגינדי. "אם אתה רואה במתמטיקה אמנות, אז זה לא כל כך נעים מבחינה אסתטית."

"מחשב יכול לעזור. זה נפלא. זה נותן לי תובנה. אבל זה לא נותן לי הבנה מלאה", הוסיף קונסטנטין. "ההבנה באה מאיתנו."

מצדו, אלגינדי עדיין מקווה למצוא הוכחה חלופית לפיצוץ באופן ידני. "אני בסך הכל שמח שזה קיים", אמר על עבודתם של הו וחן. "אבל אני רואה בזה יותר מוטיבציה לנסות לעשות את זה בצורה פחות תלוית מחשב."

מתמטיקאים אחרים רואים במחשבים כלי חדש וחיוני שיאפשר לתקוף בעיות שהיו בעבר בלתי פתירות. "עכשיו העבודה היא כבר לא רק נייר ועיפרון", אמר חן. "יש לך אפשרות להשתמש במשהו חזק יותר."

לדבריו ואחרים (כולל אלגינדי, למרות העדפתו האישית לכתיבת הוכחות בעבודת יד), קיימת אפשרות טובה שהדרך היחידה לפתור בעיות גדולות בדינמיקה נוזלית - כלומר בעיות הכרוכות במשוואות מסובכות יותר ויותר - עשויה להיות להסתמך הרבה בסיוע מחשב. "נראה לי כאילו לנסות לעשות זאת מבלי לעשות שימוש רב בהוכחות בעזרת מחשב זה כמו לקשור יד אחת או אולי שתיים מאחורי הגב", אמר פפרמן.

אם זה אכן כך בסופו של דבר ו"אין לך ברירה", אמר אלגינדי, "אז אנשים... כמוני, שיגידו שזה לא אופטימלי, צריכים להיות בשקט". זה גם אומר שיותר מתמטיקאים יצטרכו להתחיל ללמוד את המיומנויות הדרושות לכתיבת הוכחות בעזרת מחשב - משהו שעבודתם של Hou וצ'ן תספק השראה. "אני חושב שהיו הרבה אנשים שפשוט חיכו שמישהו יפתור בעיה כזו לפני שהשקיעו מזמנם בגישה הזו", אמר באקמאסטר.

עם זאת, כשמדובר בוויכוחים על המידה שבה מתמטיקאים צריכים להסתמך על מחשבים, "זה לא שאתה צריך לבחור צד", אמר גומז-סראנו. "ההוכחה [של האו וצ'ן] לא תעבוד ללא הניתוח, וההוכחה לא תעבוד ללא סיוע המחשב. ... אני חושב שהערך הוא שאנשים יכולים לדבר בשתי השפות."

עם זה, אמר דה לה לאבה, "יש משחק חדש בעיר."

בול זמן:

עוד מ קוונטמגזין