【数学】几个较好的数学定理数据库

本人的博文《人工智能的新天地：用机器证明定理》中，提到建立数学定理的数据库的必要性。

其实，除了此博文说的，建立数学定理数据库，可以为人工智能来证明数学定理提供基础之外，最现实的功能还在于，可以方便数学家们的工作，他们不必为了寻找数学文献而浪费宝贵的时间。只要手指在电脑键盘上敲几下，就可以知道围绕自己研究的题目的几乎所有的文献资料了。

本人利用周末，找到了一些比较好的数学定理数据库；尽管它们都不尽人意，只是提供了部分的时间段或几个数学领域的定理，而不是全部的定理数据库，但是至少它们开创了一些初步的工作。

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