【數學】幾個較好的數學定理數據庫

本人的博文《人工智能的新天地：用機器證明定理》中，提到建立數學定理的數據庫的必要性。

其實，除了此博文說的，建立數學定理數據庫，可以為人工智能來證明數學定理提供基礎之外，最現實的功能還在於，可以方便數學家們的工作，他們不必為了尋找數學文獻而浪費寶貴的時間。只要手指在電腦鍵盤上敲幾下，就可以知道圍繞自己研究的題目的幾乎所有的文獻資料了。

本人利用周末，找到了一些比較好的數學定理數據庫；儘管它們都不盡人意，只是提供了部分的時間段或幾個數學領域的定理，而不是全部的定理數據庫，但是至少它們開創了一些初步的工作。

1】

MathSciNet

http://www.ams.org/mathscinet/index.html

這是由美國數學學會（American Mathematical Society，AMS）根據它發行的雜誌《Mathematical Reviews》【《數學評論》】，在網上刊登了自1940年發行以來的全部數字化內容。可惜需要訂閱後才能閱讀全文；一般人員只能閱讀摘要。

2】

Cornell 大學圖書館設立的arXiv數據庫

它收集了1990年代以來的幾乎全部的數學論文。論文有摘要和全文，且似乎是對外免費開放的。除了數學，還有物理、計算機科學和生物等學科的論文。

https://arxiv.org/

數學部分：

https://arxiv.org/archive/math

3】

ProofWiki - 數學定理證明的摘要

https://proofwiki.org/wiki/Main_Page

https://proofwiki.org/wiki/Category:Proofs

4】

Metamath - 比較初等的數學定理及其證明的摘要

http://us.metamath.org/mpegif/mmtheorems.html

另外，wikipedia有一些比較重要的數學定理的證明過程：

https://en.wikipedia.org/wiki/List_of_mathematical_proofs

類似的，還有有名的MathWorld：

http://mathworld.wolfram.com/

指的一提的是，法國借政府之力，有一個非常先進的數學定理證明輔助工具Coq【法語意為"公雞"】。Coq曾被用於證明著名的“四色定理”。可惜似乎並不對外開放？

https://en.wikipedia.org/wiki/Coq

https://zh.wikipedia.org/wiki/Coq

還有一些比較專門的針對某一或某幾個數學領域設立的定理庫，這裡就不一一介紹了。

一個好消息：

國際數學聯盟【或譯“國際數學聯合會”】（International Mathematical Union，IMU）在斯隆基金（Alfred P. Sloan Foundation）的資助下，準備設立一個Global Digital Mathematics Library【全球數字數學圖書館】。消息早在2014年即已發出，不知如今進展如何。我們且拭目以待。

https://en.wikipedia.org/wiki/Global_Digital_Mathematics_Library

http://www.mathunion.org/imu-net/archive/2016/imu-net-077#c4951