人工智能的新天地:用機器證明定理
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?
https://www.quora.com/What-do-mathematicians-think-of-Metamath