幾個世紀以來，數學家們一直試圖理解和模擬流體的運動。流體方程也幫助研究人員預測天氣，設計更好的飛機，描述血液如何流經循環系統。當用正確的數學語言寫出這些方程時，它們看起來很簡單。然而，它們的解是如此複雜，以至於即使是關於它們的基本問題也很難理解。

這些方程中最古老和最突出的一個是250多年前由萊昂哈德·歐拉提出的，它描述了一種理想的不可壓縮流體的流動。幾乎所有的非線性流體方程都是從歐拉方程推導出來的。

然而，關於歐拉方程還有很多未知之處，包括它們是否總是理想流體流動的精確模型。流體動力學的核心問題之一是弄清楚這些方程是否會失敗，輸出無意義的值，使它們無法預測流體未來的狀態。

數學家們長期以來一直懷疑存在導致方程失效的初始條件。但他們無法證明這一點。

在上個月發佈在網上的預印本中，兩位數學家證明了歐拉方程的一個特定版本有時確實會失敗。這一證明標誌着一個重大突破——雖然它沒有完全解決更一般版本的方程的問題，但它給我們帶來了希望，更一般的突破最終是可以實現的。

長達177頁的論文大量使用了計算機。可以說，這使得其他數學家很難驗證它。這也迫使他們思考一些哲學問題，比如什麼是“證明”，以及如果解決這些重要問題的唯一可行方法是藉助計算機的幫助，這意味着什麼。

發現奇點

原則上，如果你知道流體中每個粒子的位置和速度，歐拉方程應該能夠預測流體將如何一直演變。但數學家們想知道事實是否如此。也許在某些情況下，方程會按照預期進行，在任何給定時刻產生流體狀態的精確值，只有其中一個值會突然飆升到無窮大。在這一點上，歐拉方程被認爲產生了一個“奇點”。

一旦它們到達奇點，這些方程就不能再計算流體的流量了。“但就在幾年前，人們所能做的還遠遠不夠（證明奇點）”，普林斯頓大學的數學家查理·費弗曼說。

如果你試圖模擬一種具有粘性的流體（所有現實世界的流體），情況就會變得更加複雜。納維和斯托克斯改進了歐拉方程，使之適用於黏性流體。他們得到的方程被稱爲納維-斯托克斯方程。到現在，數學家甚至不知道納維-斯托克斯方程是否有解。

2013年，加州理工學院的數學家托馬斯·侯（Thomas Hou）和香港恒生大學的Guo Luo提出了一種情況，即歐拉方程會導致一個奇點。他們開發了一種計算機模擬圓柱體中的流體，該流體的上半部分順時針旋轉，下半部分逆時針旋轉。當他們進行模擬時，更復雜的流體開始上下移動。這反過來又導致了沿着圓柱體邊界的奇怪行爲，在那裏相反的流體相遇。流體的渦量增長得如此之快，以至於它似乎隨時都可能“爆炸（產生奇點）”。

這一研究具有啓發性，但不是真正的證據。這是因爲計算機不可能計算出無限的值。它可以非常接近地看到奇點，但它不能真正到達奇點。如果沒有數學證明的支持，渦量的值可能只會因爲模擬的某種假像而看起來增加到無窮大。模擬會表明方程中的一個值“爆炸”了，但更復雜的計算方法會顯示相反的結果。

儘管如此，大多數數學家認爲侯和Luo的發現很可能是一個真正的奇點。但證據很難找到。

證明奇點

現在，在第一次發現奇點9年後，侯和他以前的研究生陳佳傑終於成功地證明了附近奇點的存在。

侯利用了這樣一個事實：經過仔細分析，2013年的近似解似乎有一個特殊的結構。隨着時間的推移，這些方程的解呈現出一種所謂的自相似模式，它的形狀看起來很像它早期的形狀，只是以一種特定的方式重新縮放。

在研究這個問題近十年後，加州理工學院的數學家托馬斯·侯證明，歐拉方程可以在特定情況下發展出一個奇點。現在，他把目光投向了更大的問題。

因此，數學家們不需要嘗試去觀察奇點本身。相反，他們可以通過關注更早的時間點來間接地研究它。通過以正確的速率放大解的這部分（這是由解的自相似結構決定的），他們可以模擬之後會發生什麼，包括在奇點本身。

有了一個近似的自相似解，侯和陳需要證明附近存在一個精確解。在數學上，這相當於證明它們的近似自相似解是穩定的。

但制定一個總體戰略只是解決方案的一步。繁瑣的細節很重要。在接下來的幾年裏，侯和陳花了很多時間研究這些細節，他們發現他們不得不再次依靠電腦，但這一次是以一種全新的方式。

人機合作

他們面臨的第一個挑戰是找出他們必須證明的確切命題。他們想要證明的是，如果取一組接近其近似解的值並將其代入方程，輸出不會偏離太遠。但是輸入“接近”近似解意味着什麼呢？他們必須用數學表述來說明這一點，但在這種情況下，有很多方法來定義距離的概念。

一旦他們有了描述“接近性”的正確方法，侯和陳就必須證明這一命題，這可以歸結爲一個複雜的不等式，包括重新縮放的方程和近似解的項。數學家們必須確保所有這些項的值都平衡到一個非常小的值。

爲了在所有這些不同的條件下得到他們需要的緊邊界，侯和陳把不等式分成兩個主要部分。他們可以用手工處理第一部分。第二部分需要計算機的幫助。首先，有太多的計算需要做，需要很高的精確度，這些問題對計算機來說相對容易。

但由於計算機不能處理無限數量的數字，微小的錯誤不可避免地會發生。侯和陳必須小心地跟蹤這些錯誤，以確保它們不會干擾到其他的平衡行爲。最終，他們找到了所有項的邊界，完成了證明：方程確實產生了一個奇點。

電腦證明

更復雜的方程——不存在圓柱邊界的歐拉方程和納維埃-斯托克斯方程——是否能產生奇點仍然是一個未知數。

但這至少給了我希望。我看到了一條前進的道路，甚至有可能最終解決整個千禧問題（納維-斯托克斯方程可解性問題）。

與此同時，研究人員正在研究計算機輔助證明，他們希望，計算機不僅能夠幫助解決特定流體方程的奇點問題，還能夠解決其他幾十個問題。這些努力標誌着流體動力學領域一個日益增長的趨勢：使用計算機解決重要問題。

但是在流體力學中，計算機輔助證明仍然是一種相對較新的技術。數學家們普遍認爲，一個證明必須說服其他數學家相信某條推理線是正確的。但是，它還應該提高他們對某一特定陳述爲何正確的理解，而不僅僅是提供對其正確性的驗證。還有數學家則將計算機視爲一種重要的新工具，它將使攻克以前棘手的問題成爲可能。解決流體動力學中的大問題的唯一方法，可能是嚴重依賴計算機輔助。