设万维读者为首页 广告服务 技术服务 联系我们 关于万维
简体 繁体 手机版
分类广告
版主:诤友
万维读者网 > 教育学术 > 帖子
【数学】几个较好的数学定理数据库
送交者: gugeren 2017年05月07日19:42:23 于 [教育学术] 发送悄悄话

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


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


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


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


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



0%(0)
0%(0)
标 题 (必选项):
内 容 (选填项):
实用资讯
发龙药业大回馈!美国专利骨胶原、活心素、灯盏素、排毒养颜宝购买两疗程免费邮寄中国
天天养生,保健礼品,物超所值,疯狂现金折扣,直销美加,港台,大陆,东南亚
最劲爆,最给力美国专利产品<骨精华>消除关节痛、骨质疏松<心血通>预防心肌梗塞
免开通费,30天免费试用中文电视万花筒, 无捆绑服务,月费5.99
西洋参、羊胎盘、鱼油卵磷脂200多种送礼自用健康佳品,全部特价!由此进入
留美学生医疗保险$39/月,短期访美旅游保险,不需体检无年龄限制
一周点击热帖 更多>>
一周回复热帖
历史上的今天:回复热帖
2016: 《在共匪、红魔、赤癌世界里的写照》之
2016: free, Professional VPN
2015: 再见驴十八:五七指示和爬藤
2015: 王元骏:狼性文化与Aggressive之随想
2014: 留给孩子千万财产,还不如留给他这些!
2014: 父母该如何教育人任性的孩子(转)
2013: 从数到范例-从古希腊到今中国:人类抽象