1樓：Martin awodey
同 @Felis sapiens 的答案，HoTT主要用來形式化數學裡邊最抽象的領域，比如代數拓撲，homotopy theory,範疇論等。實數是形式化的一大難點，而這個理論給出了比較優美的解決方案。目前該理論的研究熱點是如何讓HoTT中的univalence公理真正能夠計算（cubical type theory）。
2樓：金盃
多年前看到一篇程式設計師寫的文說數學語言差 王垠：數學和程式設計_程式設計師數學_酷勤網
可是我的直感是，數學理論樹基本上是無窮維的，如果以機器的思維來看，它們肯定不知道為什麼哪個地方應該長出來乙個枝條，也不知道兩個點該怎麼連在一起，尤為可怕的是，不知道什麼樣的數學命題在人類看來是有意義的，發現和抽象出一般規律的能力基本沒有。AlphaGo圍棋能下贏人，可是它依然無法生成出一條抽象出來的判斷征子或者判斷對殺的棋理，那還怎麼發展數學理論？許多數學的命題，本身必須已經是用高階概念高度抽象出來的規律才成為有意義的命題。
所以數學未來的發展肯定還是要靠人類或者真的人工智慧的，靠機器總結已有理論倒是有可能但是也非常費力……太低效了。
3樓：
數學以證明為工具, 但數學不是證明.
證明有誤不代表一定沒有價值, 證明正確也可能只是套套邏輯廢話, 甚至沒有證明都能當作有價值的猜想提出.
對數學概念作出價值判斷, 才是難上之難. 這跟其他學科, 甚至整個社會的程序都有動態鏈結. 不少有價值的數學概念, 是非數學領域的專家藉直觀或經驗觀察為基礎建立起來的.
像是辛流形等, 後來才被嚴格數學化. 數學有更多是純粹美之為美, 不是形式化壓倒一切.
會有只留意推論過程正確與否的想法, 無非是考試教育遺毒, 忽略了數學不只是正確推論跟硬套的應用. 數學也是種社會語言, 有很大程度也關乎人文素養, 甚至類似文學的美學素養
雖說如此, 也不是說涉及價值判斷跟聯絡這點, 就完全沒辦法形式化, 也是有人使用本體論ontology的方法, 去架構這種數學的概念網路, 而不涉及具體證明 http://
ontomathpro.org/ontolog
y/ , 且此方法可進一步經由其他ontology跟其他學科作鏈結的. 這產生的過程是半自動化及自然語言處理, 不是全靠人力
說到證明器, 我自己常關注 Lean prover, 但不是用來作數學研究, 只是用來證明程式正確性及跟數學概念作一定程度上的連線, 搞 Free Monad 跟 EDSL 那類東西. 暫且不管能不把整個數學變成你說的那種東西, 至少在把程式設計自動化大有可為.
4樓：Lee
我覺得這個想法很好。其實不需要電腦會證明，只要能夠檢查證明是否合法就夠了。發明一套程式語言，數學家用這套語言寫出證明過程，然後交給電腦去檢驗。
5樓：Lurker
不太明白你是啥意思，作為乙個常年做數值計算的人來看，不管現在人工智慧或是生物晶元什麼的進展如何，然而在可預見的未來中，計算機永遠是離散的，數學（大部分）和物理是連續的。計算機能做的只是逼近而已。
6樓：
說得好, 然而...你準備翻譯成什麼?
Well,你是不是覺得數學基礎就是集合論? 一切推理可以歸為謂詞演算?
誠然很多人用集合論作為基礎, 但你不能說沒有別的啊...
拿比較著名的軟體來講
Isabelle: 元邏輯引擎(FOL\HOL\ZFC\ML)
Coq: 型別論(TT)
Mathematica: 一階邏輯(FOL)
還有什麼Mizar用無型別集合論(UST), PVS用高階邏輯(HOL)...
所謂形式化是在某個體系內形式化, 體系之間, 據我所知, 不能自動轉化...
最近某會議上似乎建議數學家將自己證明的命題形式化表達一下, 不管怎麼說還是有點促進意義的.
其次形式化之後幹嘛呢? 讓機器學習怎麼證嗎?
形式化證明其實不是你想的那種一條條的證明...
怎麼說呢, 是個程式或者說是個函式...
程式即函式之組合, 函式即組合之演算, 組合即是計算, 計算即是證明.
這個難度和自動程式設計差不多
而且我覺得機器學習在定理證明上不太可能比傳統方法要好...
你用機器學習研究出來的排序演算法還能比快排快嗎?
定理證明這個東西就是高可讀性與強自動化難以並存.
適合搜尋的人沒法看, 人能看的機器搜起來慢...
高自動化低可讀性的例子: Mathematica 中公理或性質全部用一階邏輯寫一遍, 然後其他不要管了...
我啥也不用懂, 就看這個函式的值是 True or False 就行了...
證明阿貝爾群的某個性質...沒格式化就這個鬼樣,格式化後好點...
高可讀性低自動化的例子: Isabelle, 你甚至能讀出來這個過程...
但是他有個龐大的規則庫和策略集, 這玩意兒學起來可一點也不容易...
證明素數平方根不可能是有理數
7樓：
英語好的可以翻牆看這個卡內基數學系博士生的報告。
英文摘要如下：
8樓：Qinxiang Cao
問：是否有人在將既有的數學理論，都以嚴格的命題推理形式搬到電腦上來？
答：沒有。『既有的數學理論』是很龐大的體系，而且還在不斷地發展。
問：有沒有方法能夠將既有的數學理論，都以嚴格的命題推理形式搬到電腦上來？
答：有。已經有很多用於形式化證明的工具：例如Coq，Agda，Isabella/HOL等等。限於篇幅無法具體介紹他們到底是什麼。
問：基於這些工具，已經形式化了哪些重要的數學結論？
答：很多很多。我個人比較熟悉Coq上的工作。
目前初等數論已經有了比較完善的形式化。據說平面幾何也是。實數理論也有一些好用的形式化成果。
不過由於數學屆對此興趣並不大，經過形式化的成果佔整個數學理論的比例還是非常小。
另外，Yuhang Liu：是否有人在將既有的數學理論，都以嚴格的命題推理形式搬到電腦上來？中的一些說法是不對的。
固然，更高層更抽象的數學概念都應當從集合論的底層定義起來，但是這並不表示『每一步的證明的描述都要轉化為底層的集合論的語言』才能稱為形式化。
例如在Coq中，我們可以從一些初始概念來定義一些匯出概念。然後再由已經證明的初始概念的性質來證明匯出概念的性質。在形式化證明中，『更高層更抽象的數學概念及其性質』完全可以用『更高層更抽象的數學語言』簡潔的表示出來。
放棄孩子的人，在之後是否有權利將孩子要回？
tGl4 有收養協議的自然不用說！民間和電視上遇到過這樣的案例，由於親父母各種原因不能撫養 要男孩 計畫s育為了要男孩 未婚x孕等 給予他人撫養且時間長達數年，孩子有認知了，我認為沒有權利 然並卵 最後的結果無外乎 1 協商後，給撫養費要回 孩子很小 2 多次不知會直接上門，孩子二次受傷 這個見到最...
是否可以將所有人格缺陷都怪罪於父母？
文不成瘋 不可否認乙個人的性格成長 定型和身處的成長環境 社交環境有很大的關係，但私以為更重要的是乙個人的核心意志 我有個哥們，老爸好堵，一年到頭賺的錢全部搭在賭場裡面，甚至到目前為止還有外債 從小窩在家裡打遊戲 按理說這樣的成長路線長大後應該是深受其毒吧？但恰恰相反，三觀極正，待人謙謙有禮，和他相...
為什麼總有人在生活中給你加些莫須有的罪名？
Irisy 因為你很優秀，因為你和他們不一樣。很奇怪的一件事啊。年級有幾個巨好看的女孩子，從高一開始，就不停地聽說她們的 故事 豐富的感情史，美麗外表下綠茶婊的心，學藝術心術不正 熟了以後才發現，大多是杜撰的！而且，基本上都是人美又有很nice的性格，有一姑娘明明可以靠臉吃飯，成績又好出天際！所以呢...