數學證明是否是人類壓制人工智慧的最後一道防線？
如果有朝一日，人工智慧可以在數學上全面領先於人類，那人類是否就真的在智力方面完敗於人工智慧了？
上一個提法還是圍棋...
插頭
轉自wikipedia https://zh.wikipedia.org/zh-cn/%E5%9B%9B%E8%89%B2%E5%AE%9A%E7%90%86
1976年，數學家凱尼斯·阿佩爾和沃夫岡·哈肯藉助電子計算機首次得到一個完全的證明，四色問題也終於成為四色定理。這是首個主要藉助計算機證明的定理。這個證明一開始並不為許多數學家接受，因為不少人認為這個證明無法用人手直接驗證。儘管隨著計算機的普及，數學界對計算機輔助證明更能接受，但仍有數學家希望能夠找到更簡潔或不藉助計算機的證明。
為什麼對於人工智慧一定要抱著敵意呢？
如果真的有上帝般的人工智慧，那我們就是在見證一個偉大存在的誕生。即使人類被人工智慧取代了，那不也是一件很榮幸的事情？更何況，人工智慧不一定是我們的敵人，也許未來我們就是人工智慧。----------------------------------
更新下：突然被好多人點贊，之前的態度過於樂觀和狂熱會帶有一定的誤導性，本著負責的態度，我還是再補充一下吧。從歷史發展的角度來講，未來純種的人類必定會被人工智慧以及人工智慧和人類的混合體所取代。這個進程對人類來說是一場巨大的挑戰，或許會充滿血與火，沒有人能夠倖免。「幸運」的是這場對純種人類的滅種之戰，我們這一代人應該是輪不到的。
但是在這之前，我們這一代人應該會面臨自動化工具的「吃人事件「，越來越多的普通人將會失業。只有高度技術壁壘以及非邏輯性的職業能夠在這場「吃人事件」中幸免於難。但是當這麼多人失業，社會的動蕩也是必然的，在沒有誕生新的社會制度（共產主義？）之前，何談獨善其身。我糾結了好久，我想我有你想要的答案，但又不知道該怎麼回答。
我感覺這並不是你真正想要問的問題。你或許是想問，當人類引以為豪的智能都比不過人工智慧的時候，人類還剩下什麼？我可以給你一個回答：就和我們已經比不過機械的力量，比不過計算機的計算一樣，如果不考慮難度，我們也終將會比不過機器的智能。但這些都是人類的擴展。人工智慧同樣也是人類智能的擴展。不過恐怕你並不會滿足於這個答案。你可能會想問，人類被機器取代了怎麼辦？我想說的是，不會被取代。理由太長，就不解釋了。你如果真的感興趣。建議閱讀超智能體 · GitBook
讀完你就會明白人工智慧相比於人類缺少了什麼：即便是我們可以造出完美的人造智慧體，它依然缺少人類在自然選擇中所遺留在DNA中有利於生存的「慾望、恐懼、嫉妒、痛苦、好奇、怕死」等情感。這些人性是自然選擇遺留下來的有助於人類繁衍下去的關聯。也正是因為擁有這些情感，人類才會為搶奪生存資源而發動戰爭，才會因為爭奪配偶而大打出手，也才會有「害怕被人工智慧統治的恐懼」。但人工智慧不是自然選擇而來的，這些情感自然就不會產生，更不會有人類的社會道德觀念。僅僅是一個沒有慾望的工具，它們的目的也只可能是由人類來灌輸。如果未來人類真的因為人工智慧而滅絕了。並不是因為人工智慧統治人類，而是人類自己用這種人造智慧體發動了戰爭。最後我還是沒忍住想要提一下關於智能和意識關聯是智能的最小單元，01運算是計算機的最小單元。計算機通過不斷的累積這些基本運算形成高級功能，但智能是通過大量智能的並行預測形成高級智能。深層學習不得不用GPU的原因就是提高計算機的並行運算能力（但相比自然界的智能，這點並行能力遠遠不夠）。這種關聯一定是要從環境中「學習」得來，才可以隨著環境的改變而做出相應的對應（預測危險），只有這樣才能稱得上是智能。而且智能並不一定非要依附於意識。意識是智能的高級功能，為了解決一個問題：當動物獲得了移動能力之後，由於環境可變。某一時刻究竟該用哪一個預測關聯控制肢體就變成了問題（如果你在開車的時候用打籃球的預測關聯控制肢體動作，you are a dead man already）。這時就需要一個可以選擇該用哪種預測關聯的能力。再進一步形成了考慮不同環境之間的關係的能力，以此可以在複雜的環境中做出決策。也就是思考能力。意識更像是一種「監控器」。一心不可二用指的是意識。你可以同時騎車並聽歌並聊天，但的意識不可以同時出現在兩個地方（正是為了在某一時刻選擇應用哪個預測關聯）。我們睡覺的時候，意識就暫停工作，但其他智能依然並行執行。意識的大小取決於生存空間的範圍，又受限於長期記憶的能力。魚的記憶比較差，它能考慮的環境關係的能力就很弱，也就是意識的活動範圍很小。狗的意識可能由於記憶力的關係比貓能大一些。人類的生存空間是整個地球，自然是當之無愧的意識王者。我們引以為豪的，不是知道怎麼去證明，而是知道為什麼去證明
你知道四色問題嗎…
謝邀
某公司hr和我說過 圖靈機做不了數學證明 投資這一類東西
佔個坑 以後閱歷深刻再更不是。先說幾個前提：1、「缺陷」總是相對的。在文明發展的尺度上來說，如何定義「缺陷」，取決於文明發展的環境是怎麼樣的。鑒於宇宙那麼大，可以默認文明發展環境是局部動態的。
2、相比於人類，人工智慧將永遠具有「缺陷」。
關於理由，@YJango的回答已經很精彩，就個人現在的數學本科背景而言，我無法給出更系統完備的解釋。3、人工智慧可以「模擬」人類的理解模式解決問題，但無法真正「擁有」人類的理解模式。具體可參照中文房間實驗（THE CHINESE ROOM ARGUMENT）：一個對漢語一竅不通，只說英語的人關在一間只有一個開口的封閉房間中。房間里有一本用英文寫成的手冊，指示該如何處理收到的漢語訊息及如何以漢語相應地回復。房外的人不斷向房間內遞進用中文寫成的問題。房內的人便按照手冊的說明，查找到合適的指示，將相應的中文字元組合成對問題的解答，並將答案遞出房間。
約翰·希爾勒認為，儘管房裡的人可以以假亂真，讓房外的人以為他確確實實說漢語，他卻壓根不懂漢語。在上述過程中，房外人的角色相當於程序員，房中人相當於計算機，而手冊則相當於計算機程序：每當房外人給出一個輸入，房內的人便依照手冊給出一個答覆（輸出）。而正如房中人不可能通過手冊理解中文一樣，計算機也不可能通過程序來獲得理解力。既然計算機沒有理解能力，所謂「計算機於是便有智能」便更無從談起了。
（維基百科）
當然，上述中所定義的「智能」是相對狹義的。基於人工智慧無法真正「擁有」人類的理解模式，顯然人工智慧也無法擁有人類的「情感」。
2、人類壓制人工智慧還是人工智慧壓制人類可能並不是一個問題。
我的認知中，不具備「自我意識」的文明是可能存在的，但人類所創造的人工智慧是否能形成這種「無意識文明」就值得商榷了。在可預見的人類文明歷史中，即便「人工智慧」將毀滅我們的文明，也應該是作為毀滅的「工具」，而不是毀滅的「主體」。鑒於反社會人格的科學家可能多於反社會人格的政治家，「人工智慧」也許會成為比「核武器」更可怕的工具，但門檻也更高。更多的可能仍然是人工智慧作為一種輔助型工具漸漸滲透至人們的生活。鑒於人工智慧研究所涉及的領域很廣，數學，計算機，腦科學，材料學，神經科學等等，任何人工智慧研究的突破都伴隨著這些領域的發展，而這些發展所能為人類生活帶來的改變是不可估計的。人類沒有必要與「人工智慧」進行攀比。人類需要對「人工智慧」保持永遠的謹慎，並為自己的行為負責。但實際上，人類應該對自己的一切行為保持永遠的謹慎，並為自己的一切行為負責。P.S.「人工智慧」是否有擁有「自我意識」的可能性？無論現在的學界研究是什麼狀況，這種可能性當然不能被完全排除。但就目前的技術來說，不太可能。如果出現黑科技，那就另當別論。但是科技的發展永遠和人類心智相互作用，如果出現那種黑科技，人類也不是現在的人類了，或者終將不是現在的人類。早就有自動公式推導證明的程序了吧。 吳文俊（著名數學家、中國科學院院士）
有門課，叫機器證明。。。。。。。。。。。。。。。。。。。。。。。。。。。。。。。。
在一定程度上不難。
並且不需要太強的人工智慧，感覺機器學習已經夠用了。麻煩的只是數學系統和知識的編譯，不過在一些數學軟體和對應的網站里已經有了如Mathematica主要原因：很多數學證明看起來天馬行空，其實是有一定規律的。人工智慧難超越的是一些巨系統的現象，如人腦的無數神經元～但是數學的規則限制太多
對於某一類型題目的證明方向一般最多不會超過10種，再會有一些普遍的可重複的證明方法，軟體編程後一種種試，試出來的概率是很高的。比圍棋的難度要低。
當然我這裡說的題目需要很多類似的題目來提供樣本解法和證明方向。不過很多新的方法很多時候只是多種老方法的組合而已，能有這種計算力去驗證各種組合方法的只有電腦了，可能會有驚喜哦。
不過需要把程序寫好些～感覺不難的樣子，就是挺麻煩的，因為要分析題目類型，收集此類型的題目證明和相關結論，接著套個深度學習代碼吧，讓電腦自己分析規律去…數學證明的規律遠沒有社會和人心的規律複雜哦數學的問題是最簡單的，非數學的問題才是最困難的。我們對人工智慧的要求是「像人類一樣思考」，從這個意義上人工智慧永遠無法超越人類，人類智能在終點等著
真想壓制人工智慧還是應該靠哲學，來來人工智慧，我這句話是假話，一個飛速運算的CPU在每個時刻都是靜止的所以它沒有在運算，大數據少一個位元組還是大數據所以一直減到一個位元組也還是大數據，人工智慧的意識究竟存在於程序中還是數據中還是物理硬體中沒有用的，人類和人工智慧的融合，才是趨勢……我堅信，所以我早先就放棄了生物學的學習，拚命賺錢，希望有生之年能把外置大腦植入身體。總有那一天的！
先佔個坑。這個是我的專長，我來回答。
--
首先，為我占坑一年沒有回答這個話題道歉。謝謝提醒，要不然我真的忘了。
當然，這一年沒有什麼驚人的東西出現，現在回答也不晚。
首先，我們把這個問題看成兩個子問題：
A： 人工智慧數學證明發展到了什麼程度。
B： 數學證明是不是最難的問題，以至於我們會考慮為一種「壓制」人工智慧的防線。
問題A：
首先，用人工智慧證明數學定理其實不是一個新課題，很早很早其實就有ITPATP領域各種大牛在探索。但是，時至今日，我們剛剛完成了基本的定理積累。換句話說，我們其實剛收集完數據，真正的用大數據，機器學習的方法來做的序幕才剛剛拉開。本人參加了AITP的會議，Conference on Artificial Intelligence and Theorem Proving 裡面的人也是在探索階段。從這個會議上「走出來」的DeepMath等也都不是很系統的方法。大多數都還是在探索，怎麼選擇axiom這類比較基本的。現在這方面比較好的就是布拉格Joseph那個組還有奧地利的innsbruke大學吧。總之，還遠的嘞！
問題B：
當然不會是，首先首先，沒有幾個人類可以掌握那麼多定理，而且訓練一個人類科學家的成本太高太高了。所以，用大數據機器學習來做數學其實是更合理的。然後，還有很多很多問題我們沒有解決，而那些比證明定理可能難很多很多。這裡牽扯到一個proof complexity的問題。有一些的缺很難，但是整體不是不能做，而是資金和關注度都不夠。
綜上，人類擔心的太多了。
不是，是停電
233333，好嘛，毀掉圍棋後來懟數學了，下個問題我都幫你們想好了，「哲學是不是人類壓制人工智慧的最後一道防線」
感覺好多沒答到點上，請參看此書：2.7.2 NP與數學證明
數學系傷感路過.......
我覺得應該不會。
數學證明就是用已知或者已證明的當作條件去推導。會有一天，人工智慧通過智能搜索，智能統計，智能排列組合實現這一點私以為，數學證明不是，徹底擺脫人類控制才是。事實上, 數學證明, 及更一般的邏輯推理能力是人工智慧第一個歷史時期研究的內容並取得矚目的成果.
人工智慧誕生於1956年的Dartmouth會議, 之後在1956-1970年代, 人工智慧的主流研究方向便是邏輯推理. 這是因為, 很多計算機科學家是出身於數學, 並且他們認為數學家很聰明, 而數學家們能體現很高智力水平的一個重要原因是他們擁有邏輯推理能力. 那時人們認為, 一旦我們賦予機器邏輯推理能力, 機器將變得智能.
那個時期的主要貢獻是自動定理證明系統. 比如Herbert Simon和Allen Newell設計的Logic Theorist系統證明了Alfred Whitehead和Bertrand Russell的巨著Principia Mathematica裡面所有的52個定理, 並且對定理2.85發現新的且更加巧妙的證明, 這件事被記載在這本書的前言中. 另外Alfred Whitehead說這件事一定不要讓中小學生知道, 否則他們會喪失對學習數學的興趣; 以及Herbert Simon, John Shaw, 和Allen Newell設計的General Problem Solver系統, 這是一個通用問題求解系統. 在邏輯推理能力上, 機器已經取得甚至超過了人類專家的能力.
注
1. Allen Newell和Herbert Simon因此獲得了1975年的圖靈獎, 獲獎理由是: In joint scientific efforts extending over twenty years, initially in collaboration with J. C. Shaw at the RAND Corporation, and subsequentially with numerous faculty and student colleagues at Carnegie Mellon University, they have made basic contributions to artificial intelligence, the psychology of human cognition, and list processing.
2. Principia Mathematica試圖從一些公理和用邏輯推理規則出發, 使用數學證明的手段構建出整個數學基礎的大廈.
參考文獻
[1]. 周志華 著. 機器學習, 北京: 清華大學出版社, 2016年1月.
推薦閱讀：
※我們為什麼要學高數？我們為什麼要學微積分？
※如何構造悖論？
※自然科學和唯心主義是矛盾的嗎？
※行列式的本質是什麼？
※數學phd有很多內容要學習嗎？