人工智能的新天地：用机器证明定理

2016年，人工智能（artificial intelligence，AI）由于阿尔法狗（AlphaGo）战胜了人类九段围棋选手而开始成为计算机领域的热词。经过半个多世纪的发展，人工智能在语音辨认、图像辨认、有偏袒游戏（partisan game，例如国际象棋和围棋）、书面语言翻译等方面都有了飞速的发展，可以与人类的智慧媲美了。

接下来，本人认为，人工智能将在自动化定理证明方面大展身手了。

自动化定理证明（Automated theorem proving，ATP）是计算机自动推理和数学逻辑的下属领域。它通过计算机程序来证明数学等学科的定理。

目前需要做的工作：

1】整理和正规化数学各分支的定义、引理和定理，用类似人类自然语言的计算机语言来建立这些定义、引理和定理的数据库。这种数据库目前已经存在多种，但是规格不统一，调用不容易，内容也不规范（例如，没有显示出各个定理之间的逻辑关系）。

2】这种定理数据库，应该

--不但可以描述定义、引理和定理的内容，而且可以从某个/某些条件产生出相关的定义、引理和定理的结论，更可以提示这些条件下可能得出的其他相关的结论。

--可以把各种数学分支之间、各种定义、引理和定理之间的逻辑关系梳理清楚。

==

相关链接：

自动化定理证明（Automated theorem proving，ATP）

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

Metamath是一种写定理数据库的语言和数据库

http://us.metamath.org/

What do mathematicians think of Metamath?