1. 數學研究1.1. 數學研究變得更爲艱難了1.1.1. 學科分支越發密集，問題越發複雜1.1.2. 攻讀博士學位的3年時間，只夠去理解導師所給題目的含義1.1.3. 隨後，再花費數年時間去研究、探索，運氣不錯的話，會得到一些研究成果1.1.4. 然而，你發表的論文卻面臨著沒人能審核它1.2. 審核別人發表的論文是得不到太多報酬的，但期刊論文的審核必須經過同行的評審1.2.1. 有一個像Coq證明助手這樣的系統就非常重要了1.3. 數學的發展雖然受到人類大腦局限性的制約，但借助于計算機，我們對數學的探索已遠遠超出了人腦的思維範疇1.3.1. 如果很難找到通往“新奇迹”的方向，人們終將失去創造的原動力1.4. 費馬大定理的證明長達數百頁，跨越3個世紀，這說明人類擁有足夠的耐心1.4.1. 當你努力去證明一個極其複雜的猜想時，隱約會有一種突破人類大腦物理極限的感覺1.4.2. 數學是無限的，而人的能力是有限的1.4.3. 我們常會爲自己所做的努力感到吃驚，因爲我們用數學的方式證明了“數學海洋的廣闊無邊”1.4.4. 鑒于我們可能即將觸及人類自身能力的極限，一些數學家已意識到，如果希望人類文明持續進步，我們將需要更多的機器輔助1.5. 奧地利數學家、邏輯學家庫爾特·哥德爾（Kurt Gödel）有過論證：數學中包含了許多沒有經過證明的真理1.5.1. 人們創造出了一套龐雜且仍在擴展的公理系統，但人們研究它的目的越來越說不清楚1.5.2. 數學家是將咖啡轉化爲定理的機器。1.5.2.1. 著名的匈牙利數學家保羅·厄多斯1.6. 數學家只用鉛筆和紙張工作的日子即將結束1.6.1. 以色列數學家多倫·澤爾伯格（Doron Zeilberger）1.6.2. 人們之所以不願倚重人機合作的方式，是因爲“狹隘的人本主義”在作祟，這種偏執與其他形式的偏執一樣，阻礙了人類發展的腳步1.6.3. 人類再也不可能僅使用筆和紙來探求數學的奧義了1.7. 不僅希望能得到真理，並且希望探求真理背後更多的內涵1.7.1. 如果計算機在無法真正理解數學的情況下就能驗證數學真理，他們會覺得非常荒謬1.7.2. 我們的理想是探究數學真谛，而不是利用機械執行指令的計算機推演論證1.7.2.1. 菲爾茲獎的數學家邁克爾·阿蒂亞（Michael Atiyah）1.8. 在數學領域裏，利用計算機完成很多工作已經變成現實1.8.1. 現在，人類很多剛發表的論文就已過時了，其實完全可以用算法來替代人類完成這些工作1.8.2. 現如今我們遇到的很多問題已經變得毫無意義，但是我們還是繼續在做，僅僅因爲這是人類可以做的事情1.8.3. 爲了做某事而做某事所帶來的意想不到的成果已經多次證明，無目標驅動的研究有時是收集真正的新見解的最佳方式1.9. 我們非常擅長搞定計算機無法做到的事情1.9.1. 如果目前所知道的一切定理都可以通過計算機得到證明，那我們就可以去探索計算機無法解決的其他問題，這有可能成爲未來的“數學”1.9.2. 人類的許多研究成果不是向前而是橫向平行延伸的1.9.3. 在某些領域我們確實達到了臨界點，想要超越珠穆朗瑪峰的高度就必須借助一台機器2. 弗拉基米爾·沃沃斯基2.1. Vladimir Voevodsky2.1.1. 明星數學家，他僅用傳統的紙筆工具就在數學研究領域成績斐然，但後來他開始倡導數學家使用計算機技術輔助研究工作2.2. 沃沃斯基認爲安非他命能使他産生大量幻覺，可以使他激發出極大的靈感2.2.1. 正常蜘蛛可以迅速織出形狀規則的網，而攝入咖啡因的蜘蛛織的網就像一團亂麻2.3. 兩個危機2.3.1. 涉及“理論數學”和“應用數學”的分離2.3.1.1. 沃沃斯基極其重視向外界闡述他所從事的研究工作將來會對社會産生的深遠影響2.3.2. 另一個危機更像是一場生存危機，它與數學研究變得日益複雜有關2.3.2.1. 即使數學家們能夠精通各自研究的細分領域，但對他人的研究過程和成果缺乏足夠的了解2.3.2.2. 沃沃斯基認爲，如果人類無法檢驗彼此的證明成果，那麽我們可能需要尋求機器的幫助2.3.2.3. 大多數數學家繼續堅信，在自身敏銳直覺的引導下，人類思維才是促進方程和幾何研究發展並可獲得解決方法的核心力量2.3.2.3.1. 談論使用計算機輔助研究似乎就是誤入歧途2.4. 同時化解兩個危機的方法2.4.1. 他發現看似呆板機械的數學範式竟然完美地構建了計算機世界2.4.2. 他可以利用這種“新語言”來創建一套全新的研究數學領域的基礎方法，計算機將在其中發揮核心作用2.5. 學術期刊的論文遲早會由于過于複雜而無法得到詳細的論證，而這將導致期刊文獻中出現未檢測到的錯誤2.5.1. 數學是一門深度學科（具有複雜的層階結構），一篇論文通常將之前許多篇論文的結論作爲依據，這種錯誤的疊加效應將會得到非常危險的結果2.5.2. 他發現唯一可行的計算機系統是法國的Coq系統，它能夠引導證明2.6. 他致力于研究數學如何避免發生潛在災難的問題2.6.1. 運用數學方法來解決其他領域的問題2.6.2. 他發現自己並沒有深入探究生物學問題的工具和技能2.7. 如果你想要深入了解某些知識和概念，就試著備課並教會別人2.7.1. 計算機學者所使用的程序設計語言，起初看似難懂，實則是他早些年作爲數學家時運用過的一種抽象世界的範式2.8. 那些仍用紙筆計算的學者（可能現在也使用計算機來檢驗常規計算結論）和那些想用計算機來證明新定理的學者之間仍然存在較大分歧2.8.1. 雖然使用計算機檢查證明結論的方法正在被更多人接受，但數學研究的方向和方法依然掌握在人類手中2.8.2. 計算機還不具備在數學研究領域的獨創能力2.9. 新的數學研究方法首先會被一小部分人運用，然後逐漸普及，最終成爲標准，緊接著就會出現在數學專業研究生的課堂上，進而推廣到本科教育階段2.9.1. 這個過程大約需要幾十年，接下來會發生什麽就不得而知了