人工智能的新天地：用機器證明定理

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?