計算機科學家告訴數學家如何撰寫證明

本文發表於《大眾科學》的前部落格網路，反映了作者的觀點，不一定反映《大眾科學》的觀點

信不信由你，我確實有一些朋友會說他們不喜歡數學，他們時不時地會在 Facebook 上分享這個梗圖：然後撒旦說：“把字母表放進數學裡。” 每次這個梗圖出現時，背景圖片都不同，但文字總是相同的。有些人覺得抽象符號是數學課開始讓他們感到困惑的地方。

但是如果我們沒有那種符號呢？在本學期我的數學史課上，我們瞭解了在我們（撒旦？）將字母表放入數學之前，數學是什麼樣的。具體來說，我們和花拉子米一起完成了配方法，這位波斯數學家撰寫了關於求解線性和二次方程的教科書，這本書給了我們“代數”這個詞。他沒有使用符號來表示未知量，所以他的書中包含這樣的說明

“一個平方和 10 個根等於 39 個單位。因此，這類方程中的問題如下：哪個平方與它的十個根組合起來會得到總和 39？解決這類方程的方法是取剛才提到的根的一半。現在我們面前的問題中的根是 10。因此取 5，它自身相乘得到 25，將這個量加到 39 得到 64。然後取它的平方根，即 8，從中減去根的一半，5 剩下 3。因此，數字三代表這個平方的一個根，它本身當然是 9。因此，九給出了平方。”

關於支援科學新聞

如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞事業 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。

今天，我們會將該段落翻譯成這樣

x²+10x=39。求 x²。

x²+10x+5²=39+5²

(x+5)²=64

x+5=8

x=3

x²=9

我認為我們大多數人，包括我那些對數學有恐懼症的 Facebook 朋友，都會發現第二個版本更容易理解和遵循。正如我對我的班級所說，唯一比在數學中使用字母表更糟糕的事情是在數學中不使用字母表。

本週，我正在參加海德堡桂冠論壇，這是一個類似於林道諾貝爾獎獲得者論壇的數學和計算機科學論壇，並且為論壇部落格撰寫文章。週二，萊斯利·蘭波特，他在 2013 年獲得了計算機科學領域的圖靈獎，做了一個題為“如何撰寫 21 世紀的證明”的演講，演講的開頭與我的歷史課和我所做的觀察相同：公式比散文方程更容易閱讀和解析，所以當我們在撰寫關於數學的文章時，我們已經超越了散文方程。那麼，為什麼數學家堅持用散文來撰寫證明，就像 17 世紀的數學家那樣？

萊斯利·蘭波特身穿一件寫著“你想要證明？我會給你證明！”的 T 恤衫在海德堡桂冠論壇上做了演講。圖片來源：HLFF/Kreutzer。

當我看到演講的標題時，我以為蘭波特會談論計算機證明檢查程式，甚至是像蒂莫西·高爾斯所研究和撰寫的那樣的證明建立程式。但蘭波特的建議要實際得多。他實際上是在描述一種讓數學家撰寫更容易閱讀且更難出錯的證明的方法，這種方法可以替代冗長的散文證明。“當你撰寫證明時，你試圖做兩件事，”蘭波特在稍後與媒體的會議上說。“一方面，你想展示某些東西是美麗的，但另一方面，你試圖證明它是真實的。真理可能是美，美可能是真理，但你不能用同樣的方式來證明它們。”

他的方法，您可以在他的網站上閱讀更多詳細資訊 (pdf)，是一種分層結構，它看起來與我們大多數人在初中或高中幾何課上學到的雙欄證明並沒有完全不同，儘管他指出它可以處理在這種雙欄格式中會顯得笨拙的複雜問題。每行都編號，並且每個斷言都用引用前幾行和斷言的數字來證明。

蘭波特引用了邁克爾·斯皮瓦克的微積分教科書：“……精確性和嚴謹性既不是對直覺的阻礙，也不是目的本身，而是構建和思考數學問題的自然媒介。” 然後，他帶領我們瀏覽了該教科書中值定理的推論的證明，指出了他認為不夠精確或嚴謹的陳述，並使用他的技術重寫了證明。

蘭波特說，他的技術的好處不僅在於，甚至主要不在於它對讀者的價值。它也是一種更好的方法，可以找到自己工作中的錯誤，並防止它們進入已發表的作品。儘管他承認確切的總體數字尚不清楚，但他表示，在一項小型研究中，1/3 已發表的、經過同行評審的數學論文包含錯誤的定理。其中一些是錯誤的，因為證明是錯誤的，而另一些是錯誤的，因為它們依賴於錯誤的證明。無論原因如何，錯誤的定理都不應該發表，蘭波特說他的證明結構使我們不會讓草率的思維侵入我們的寫作。（海德堡桂冠論壇的聯合博主馬庫斯·珀塞爾也撰寫了關於蘭波特演講的文章，並擴充套件了他關於清晰寫作的一些想法。）

蘭波特建議，如果期刊堅持只發表“17 世紀”的證明，數學家也應該無論如何都寫出來，以此來確保證明是萬無一失的。作者可以將分層證明發布在其網站上，或許可以使用超文字來允許讀者隱藏或顯示每個步驟中的詳細資訊，或者在證明的每個步驟中包含主要思想的摘要。

在與媒體的會議上，蘭波特談到了這項技術的另一個好處，他在演講中沒有時間談到。他說，一旦你有了分層證明，你就可以很容易地在新證明中使用它的片段。例如，如果你想稍微改變一個假設或專注於具有不同屬性的解決方案，你將能夠很容易地分辨出證明的哪些部分可以保持不變，哪些部分需要改變。

這次演講引發了很多問題，我聽到與會者整天都在討論它。並非所有在場的數學家都對一位計算機科學家（即使是一位擁有數學博士學位和圖靈獎的計算機科學家）告訴他們如何撰寫證明感到興奮。他們中的一些人強烈地認為，分層證明會損害他們作品的美感。有些人認為，這種技術可能適用於教學環境中的簡單證明，但不可能適用於研究環境中的更復雜證明。我認為蘭波特會爭辯說，如果你認為你不能以這種形式撰寫你的證明，那麼你對證明的理解還不夠。

就我個人而言，我發現蘭波特的論點很有說服力。用文字解釋的代數方程和用符號解釋的代數方程在清晰度上的差異就像白天和黑夜一樣，如果蘭波特是對的，那麼切換到這種證明技術會引起類似的清晰度飛躍。改變是困難的，但我對它對我教學、思考和溝通的潛在好處很感興趣。

這篇博文源自第二屆海德堡桂冠論壇 (HLF) 的官方部落格，該論壇於 2013 年 9 月 21 日至 26 日在德國海德堡舉行。24 位阿貝爾獎、菲爾茲獎和圖靈獎得主將齊聚一堂，會見 200 位年輕研究人員的精選小組。